Questions tagged [proof-assistants]
A proof assistant is software used for creating and checking formal proofs; examples include Coq and HOL. This tag is not to be used for requesting assistance on finding proofs. General questions about proof assistants can also be asked on the Proof Assistants Stack Exchange site.
20
questions
152
votes
5
answers
27k
views
What makes dependent type theory more suitable than set theory for proof assistants?
In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he ...
- 1,617
99
votes
2
answers
11k
views
Extent of “unscientific”, and of wrong, papers in research mathematics
This question is cross-posted from academia.stackexchange.com where it got closed with the advice of posting it on MO.
Kevin Buzzard's slides (PDF version) at a recent conference have really ...
137
votes
28
answers
18k
views
Which mathematical definitions should be formalised in Lean?
The question.
Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?
Examples.
In the current stable version of the Lean Theorem Prover, topological groups ...
58
votes
8
answers
12k
views
How true are theorems proved by Coq?
Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...
- 33.9k
24
votes
3
answers
2k
views
What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
Over the years, advances in machine learning has allowed us to communicate and interact, using the same natural language, more and more semantically with computers, e.g. Google, Siri, Watson, etc. On ...
13
votes
3
answers
2k
views
Is there research on Machine Learning techniques to discover conjectures (theorems) in a wide range of mathematics beyond mathematical logic?
Although there already exists active research area, so-called, automated theorem proving, mostly work on logic and elementary geometry.
Rather than only logic and elementary geometry, are there ...
- 325
7
votes
1
answer
1k
views
Set-theoretic tautologies
Let us consider unquantified formulas of a set theory (for example, NBG), more precisely,
the formulas, constructed from variables and the constants $\emptyset, V$ (the empty set
and the class of all ...
- 897
152
votes
6
answers
16k
views
Proofs shown to be wrong after formalization with proof assistant
Are there examples of originally widely accepted proofs that were later discovered to be wrong by attempting to formalize them using a proof assistant (e.g. Coq, Agda, Lean, Isabelle, HOL, Metamath, ...
81
votes
4
answers
7k
views
Wanted: a "Coq for the working mathematician"
Sorry for a possibly off-topic question -- there are four StackExchange subs each of which could be construed as the proper place for this question, and I've just picked the one I'm most familiar with....
- 33.2k
72
votes
13
answers
10k
views
The use of computers leading to major mathematical advances II
I would like to ask about recent examples, mainly after 2015, where experimentation by computers or other use of computers has led to major mathematical advances.
This is a continuation of a question ...
58
votes
9
answers
8k
views
How do they verify a verifier of formalized proofs?
In an unrelated thread Sam Nead intrigued me by mentioning a formalized proof of the Jordan curve theorem. I then found that there are at least two, made on two different systems. This is quite an ...
- 32.1k
47
votes
5
answers
8k
views
Proof assistants for mathematics
This question is related to (maybe even the same in intent as) Intro to automatic theorem proving / logical foundations?, but none of the answers seem to address what I'm looking for.
There are a lot ...
37
votes
1
answer
4k
views
How much mathematics has been formally verified?
That's a vague question so allow me to tighten it up a bit.
I recently noticed that there is a formal machine verified proof of the Central Limit Theorem (CLT) implemented with Isabelle. This ...
- 8,106
33
votes
4
answers
4k
views
What is the endgoal of formalising mathematics?
Recently, I've become interested in proof assistants such as Lean, Coq, Isabelle, and the drive from many mathematicians (Kevin Buzzard, Tom Hales, Metamath, etc) to formalise all of mathematics in ...
29
votes
4
answers
5k
views
Why is it so difficult to write complete (computer verifiable) proofs?
For example I have read that is agony to give a complete proof of the Jordan curve theorem. Since all statements are meant to be justified by the postulates, where does the difficulty lie?
- 4,261
16
votes
1
answer
2k
views
Axioms of Choice in constructive mathematics
There is a widely accepted opinion that the Axiom of Countable Choice (further, ACC)
$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \...
- 781
10
votes
0
answers
307
views
Feferman's universes for proof assistants?
This question was prompted by a discussion from another MO question about the consistency of ZFC. There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them,...
- 78.7k
6
votes
3
answers
1k
views
Proof formalization
I read some time ago some papers about proof formalization. Typically, I began whith this one, from Lamport.
Are there more recent works in this field ?
2
votes
2
answers
944
views
How to interpret conflicting formal proofs about "a mod 0 = ? "
The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$.
According to Coq
$$ a \mod 0 = 0$$
and Isabelle proves
$$ a \mod = a$$
...
- 24.2k
0
votes
1
answer
380
views
How bad is Coq proving both $T$ and $\lnot T$? [closed]
Question: How bad is Coq proving both $T$ and $\lnot T$? Can it be abused?
Back in 2011 on the coq-club mailing list there was a thread:
Is the Daniel Schepler's inconsistency real?.
In the thread ...
- 24.2k