Automated theorem proving ​

Lean is great. Kind looks awesome too.

Links ​

• Architecture of proof assistants (2018)
• Vampire - Theorem prover, that is, a system able to prove theorems. More precisely, it proves theorems in first-order logic. (Code)
• hout - Non-interactive proof assistant using the Haskell type system.
• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• XPath-like Query Logics: Proof Systems and Real-World Applicability (2019)
• Abella - Interactive theorem prover based on lambda-tree syntax. (Code)
• Poi - Pragmatic point-free theorem prover assistant. (HN)
• STP - Simple Theorem Prover, an efficient SMT solver for bitvectors.
• Posts in the category "Every proof assistant"
• Graph Representations for Higher-Order Logic and Theorem Proving (2019) (HN)
• Generative Language Modeling for Automated Theorem Proving (2020) (HN)
• Untangling Mechanized Proofs (2020) (HN)
• SASyLF - Educational Proof Assistant for Language Theory. (Code)
• Automated Propositional Sequent Proofs in Your Browser with Tau Prolog (2021)
• Proof-Oriented Programming in F*
• HipSpec - Inductive theorem prover for Haskell programs.
• Twee - Equational theorem prover based on Knuth-Bendix completion.
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (2019)
• Cicada Language - Dependently typed programming language and an interactive theorem prover.
• Holbert - Graphical interactive proof assistant designed for education.
• Rusty Razor - Tool for constructing finite models for first-order theories.
• Timothy Gowers's research on automated theorem proving
• Pocket-Prover - Fast, brute force, automatic theorem prover for first order logic.
• homotopy-rs - Proof assistant allows the construction of composite morphisms in a finitely-generated semistrict n-category, via a point-and-click user interface.
• Proof Assistant Demos
• Incredible Proof Machine - Non-textual interactive theorem prover. (Web)
• The future of interactive theorem proving? (2022) (HN)
• Functional Benchmarks - Collection of benchmarks of functional programming languages and proof assistants.
• PML - Language provides a uniform environment for programming, and for proving properties of programs in an ML-like setting.
• AUTO2 - Best-first-search theorem prover implemented in Isabelle.
• Tutorials and courses for Z3
• Proost - Simple proof assistant written in Rust.
• HOL Light theorem prover