“Papers With Computer-Checked Proofs”, Daniel J. Bernstein2023-09-07 (crypto, math)⁠:

This report gives case studies [in Lean & HOL Light] supporting the hypothesis that it is often affordable for a paper presenting theorems to also include proofs that have been checked with today’s proof-checking software.

[Keywords: mathematics, proofs, formalization, computer verification, computer assistance, human time]

See Also:

• Social Processes and Proofs of Theorems and Programs

• How to Write a 21^st Century Proof

• STEPS Toward Expressive Programming Systems: “A Science Experiment”