Questions tagged [formalization]

Questions on the computer-formalisation of mathematics, in proof assistants and related software

4 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
7 votes
0 answers
584 views

Theorem proving in Lean, for areas that aren't quite ready for it

While taking a break from being stuck, I have found myself addicted to playing with the Lean Theorem Prover. (Beware, if you visit this link might you might find yourself hooked...) Playing with this ...
Jon Bannon's user avatar
  • 6,977
4 votes
0 answers
137 views

Formal and informal proofs: Is there any "bilingual corpus"?

There are extensive libraries of formalized mathematics like those of Lean, Coq or Isabelle/HOL. What I am interested in is documents of formalized mathematics that closely follow certain informal ...
Marcos Cramer's user avatar
3 votes
0 answers
238 views

Research on formalization of what constitutes a good theorem

This question is about automating theorem proving. Now automated theorem proving, as currently understood in CS literature, has little to do with pure mathematics as practiced on this site (I believe ...
user avatar
1 vote
0 answers
38 views

Does there exist a database of formalized definitions and theorems based on NBG set heory?

Is there a library of formalized mathematical definitions and theorems similar to Lean's mathlib, but based on Von Neumann–Bernays–Gödel set theory and first order logic, rather than type theory? I am ...
Zsombor Kiss's user avatar