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
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
25
votes
3
answers
385
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, ...
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
23
votes
4
answers
513
views
To what extent is formalized mathematics publishable?
I am interested in contributing to the formalization of mathematics, but I don't know the extent to which such activities are publishable. Here are some questions in this vein:
How can one determine ...
- 981
22
votes
1
answer
577
views
How hard is computing integrals in Lean?
Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level ...
- 1,058
20
votes
1
answer
312
views
Examples of formalisation of abelian categories
The question
I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
- 2,500
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,058
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
16
votes
1
answer
552
views
Proof assistants and formalised mathematics in the MSC database
I was looking at the MSC2020 database and I find it hard to identify a field suitable for works about proof assistants and formalised mathematics. 03B70 ("Logic in Computer Science") might ...
14
votes
4
answers
320
views
Algorithms obtained through constructive formalization
Formal proofs in proof systems that avoid the law of the excluded middle and certain other principles can be automatically converted into algorithms.
What useful new algorithms have been produced by ...
- 901
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
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$ ...
- 367
13
votes
1
answer
161
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 ...
- 901