Skip to main content

Questions tagged [history]

The history of proof assistants and machine-assisted proofs.

Filter by
Sorted by
Tagged with
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 ...
24 votes
2 answers
600 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 ...
4 votes
0 answers
104 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 ...
13 votes
0 answers
365 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-...
7 votes
3 answers
406 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 ...
8 votes
1 answer
200 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 ...
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 ...
12 votes
2 answers
576 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 ...
14 votes
4 answers
318 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 ...
12 votes
2 answers
202 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 ...
15 votes
4 answers
391 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 ...
25 votes
3 answers
863 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?
22 votes
3 answers
625 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 ...
9 votes
1 answer
123 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$ ...