# 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