Skip to main content

Questions tagged [history]

The history of proof assistants and machine-assisted proofs.

Filter by
Sorted by
Tagged with
25 votes
3 answers

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?
taylor.2317's user avatar
  • 1,318
24 votes
2 answers

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 ...
Will Sawin's user avatar
22 votes
3 answers

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 ...
Jason Rute's user avatar
  • 8,620
15 votes
4 answers

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 ...
Greg Nisbet's user avatar
  • 2,761
14 votes
4 answers

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 ...
Will Sawin's user avatar
13 votes
0 answers

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-...
user21820's user avatar
  • 484
12 votes
2 answers

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 ...
Julian's user avatar
  • 576
12 votes
2 answers

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 ...
Jason Rute's user avatar
  • 8,620
11 votes
6 answers

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 ...
tryst with freedom's user avatar
9 votes
1 answer

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$ ...
John's user avatar
  • 367
8 votes
1 answer

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 ...
user833970's user avatar
7 votes
3 answers

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 ...
Ana Borges's user avatar
6 votes
3 answers

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 ...
Jason Rute's user avatar
  • 8,620
4 votes
0 answers

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 ...
Trebor's user avatar
  • 3,927