Questions tagged [mathematics]
Use this tag for questions a mathematician would feel at home answering and can be traced back to an area of mathematics.
22
questions
18
votes
2
answers
401
views
How can I prove facts about floating point calculations?
In computing, there is a standard called IEEE 754. Unlike in mathematics, computers have to fit numbers into a finite amount of space; to do this, they use a format a bit like scientific notation, ...
- 1,112
12
votes
2
answers
123
views
Proof assistants with dynamic scope/local instances/etc.?
Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and ...
- 221
13
votes
1
answer
180
views
Representing $\Bbb RP^2$ in Lean: building a type representing a particular set
I need to work with the set of all lines in the Cartesian plane. For my context, the natural way to think of this is that a line can be described by an equation $Ax + By + C = 0$, where $A$ and $B$ ...
- 166
27
votes
8
answers
961
views
Where can I find lists of theorems that have been verified?
I recall many years ago seeing a very large and well-interlinked (by computer) list of verified results starting from base assumptions and leading to all sorts of things that naive me did not expect ...
- 406
20
votes
0
answers
275
views
Can we automatically get around set-theoretic difficulties?
One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
- 1,013
13
votes
1
answer
162
views
Exotic natural language summaries of formal proofs
Mathematical proofs written in natural language can often be used as guides to create formal proofs in proof assistants, depending on the level of detail of the proof and how many results and concepts ...
- 146
25
votes
3
answers
386
views
Examples of new mathematics discovered through formalization?
In his essay Why formalize mathematics?, Patrick Massot discusses several reasons behind why a working mathematician might be interested in proof formalization. One of the the reasons he discusses is, ...
CommunityBot
- 1