Questions tagged [history]

The history of proof assistants and machine-assisted proofs.

Filter by
Sorted by
Tagged with
8 votes
1 answer
155 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 ...
user avatar
10 votes
0 answers
149 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-...
user avatar
  • 421
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 ...
user avatar
  • 3,355
14 votes
4 answers
262 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 ...
user avatar
11 votes
2 answers
351 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 ...
user avatar
  • 3,355
20 votes
3 answers
281 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 ...
user avatar
  • 3,355
9 votes
1 answer
99 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$ ...
user avatar
  • 285
21 votes
2 answers
212 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 ...
user avatar
13 votes
2 answers
163 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 ...
user avatar
  • 566
16 votes
4 answers
287 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 ...
user avatar
  • 2,477
25 votes
3 answers
598 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?
user avatar
  • 1,182