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.
6
questions
46
votes
2
answers
2k
views
Are some proof assistants better suited for given areas of math than others?
There are many different proof assistants out there, and I think it is reasonable to expect that more or less all results we prove in everyday mathematics can be proven in any of them. One nice way to ...
- 1,058
27
votes
8
answers
945
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 ...
26
votes
2
answers
1k
views
What set-theoretic definitions can't easily be formalized in a type theory?
Most proof assistants (with some exceptions like Isabelle/ZF or the B method) rely on type theory.
See also the MathOverflow question What makes dependent type theory more suitable than set theory for ...
- 406
18
votes
2
answers
393
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, ...
- 495
24
votes
2
answers
766
views
Why haven't all of the "hundred greatest theorems" been formalized yet?
The "hundred greatest theorems" used to be maintained here.
See this page for the current status of the formalization of these theorems.
Apparentely, Fermat's Last Theorem, the Isoperimetric ...
- 981
13
votes
2
answers
205
views
verifying combinatorial constructions - choice of a proof assistant
The choice of the proof assistant to use for formalisation depends on the area quite a bit; e.g. they say that algebraic topology comes easy in HoTT assistants.
What would be the most natural choices ...
- 480