Skip to main content

Questions tagged [history]

The history of proof assistants and machine-assisted proofs.

Filter by
Sorted by
Tagged with
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-...
user21820's user avatar
  • 484
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?
taylor.2317's user avatar
  • 1,318
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 ...
Jason Rute's user avatar
  • 8,620
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 ...
Greg Nisbet's user avatar
  • 2,761