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
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 ...
12
votes
3
answers
521
views
Why are impredicative constructions used less in type theory than in material set theory?
Many infinitary objects in (say) ZFC are constructed with impredicative principles. The natural numbers are formed by intersecting every inductive set (whose existence is given by the axiom of ...
- 5,510
0
votes
0
answers
53
views
Correcting formally verified results
John Harrison spoke once about checking the results of some peer reviewed mathematical research: he has found bugs in the proofs and even a faulty theorem, which he corrected by giving a formal proof.
...
- 321
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 ...
- 2,500
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,290
5
votes
0
answers
1k
views
What's the general idea (intuition) behind Andrej's topos where reals are countable? [closed]
I am very surprised that Andrej Bauer claimed to have found a topos where reals are countable. He said it'll take a month to write down the proof, and I think that's very understandable.
However, I'm ...
- 9,732
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 ...
- 9,150
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 ...
- 2,053
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 ...
- 9,150
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 ...
- 3,200
2
votes
2
answers
206
views
What is known about minimal sets of axioms? [closed]
There are several axioms that are known to be independent of the usual ones; for instance, the Axiom of Choice. This axiom can be stated in several equivalent ways, e.g.:
For every set $A$, $\mathcal{...
- 351
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 ...
- 731
8
votes
1
answer
127
views
Have the common algorithms in existing computer-assisted proofs been transitioned to proof assistants?
In my experience, one of the most common applications of computer-assisted proofs in math is establishing that a given system of constraints is infeasible. Here are some examples of settings and tools ...
- 480
8
votes
1
answer
152
views
What are some useful resources for a mathematician interested in learning Isabelle/HOL?
What are some useful and reliable resources for a mathematician interested in learning Isabelle/HOL? Could be online (websites) or physical (books).
- 2,846
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 ...
- 9,150