Questions tagged [history]
The history of proof assistants and machine-assisted proofs.
14
questions
11
votes
6
answers
3k
views
Have ideas from programming helped us create new mathematical proofs?
Other than trivial ones where computers checked all cases by brute force, have programs led us to find new proofs? Since programming has been it's own field for long, I suppose there must be some ...
4
votes
0
answers
81
views
Independence of function extensionality
Who first realized that function extensionality cannot be proved within vanilla MLTT, or some variations of it? Now to my knowledge the simplest way to show this is by syntactic models. But surely ...
- 3,678
7
votes
3
answers
349
views
Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug?
Critical bugs are periodically found in Coq, and I assume in other proof assistants as well. We are still happy to mostly trust the proof assistants, partly because these critical bugs are relatively ...
- 886
8
votes
1
answer
190
views
What should be cited for "the Calculus of inductive Constructions"?
The history of dependent data types spans decades and is a bit confusing. I have seen some implausible claims about which documents present what. I would like to get it right for my own work without ...
- 433
13
votes
0
answers
322
views
Unintentionally proven false theorem with type-in-type outside logic and foundations?
We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
- 455
6
votes
3
answers
3k
views
What are good examples of April fools jokes in the proving assistant community?
Every community can have inside jokes among it, and April Fool’s jokes are a common variety, but proof assistants are particularly susceptible to April Fool’s jokes. They have strong guarantees of ...
- 6,713
14
votes
4
answers
298
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 ...
- 891
11
votes
2
answers
489
views
How does the formal proof of the four color theorem work?
Over a decade ago, Georges Gonthier, gave a formal proof of the four color theorem. I have a mental picture of how the proof works, and I'd like to see if it is correct.
The original proof of the ...
- 6,713
21
votes
3
answers
499
views
Impact of "Formalizing 100 Theorems" and what is next
In the early 2000s (or maybe even earlier) Freek Wiedijk published a list of 100 theorems which were a sort of litmus test of the state of the art in formalized mathematics. As the completion rate ...
- 6,713
9
votes
1
answer
116
views
How did the meaning of "lifting" in proof assistants arise?
In topology, the notion of "lifting" has a quite a long history, starting with the theory of covering spaces, where the classic example is that if you take an outdoor spiral staircase, $S$ ...
- 315
23
votes
2
answers
481
views
Successes of machine learning in formal theorem proving
Attempts to apply machine-learning (as opposed to hand-crafted automation) to formal theorem proving are still in their infancy.
Still, there have been some successes. GPT-f found some proofs that ...
- 891
12
votes
2
answers
190
views
Are there any proof assistants which integrate JITs?
Has there been notable research or attempts to integrate a JIT compiler into a proof assistant in order to achieve performance gains for proof verification, or general programming?
Whilst it may seem ...
- 566
15
votes
4
answers
368
views
Are there any well-known Internal DSL Proof Assistants?
Proof assistants like Coq have their own extensible syntax that's rather different from a general purpose language.
I'm curious whether there are any well-known proof assistants that are implemented ...
- 2,681
25
votes
3
answers
778
views
What was the 1st Proof Assistant?
What was the first proof assistant? What was it used for? When and by who was it created? Is it still used today? And what was its purpose?
- 1,288