Everything I know
π‘
π¦
π
π·
Searchβ¦
README
Meta
Sharing
Ideas
Focusing
Minimalism
Research
Knowledge
Environment
Music
Life
Writing
macOS
Hardware
Math
Logic
Combinatory logic
Satisfiability modulo theories
Automated theorem proving
Lean
Linear algebra
Lambda calculus
Real Analysis
Type Theory
Category theory
Statistics
Mathematical optimization
Geometry
Geometric Algebra
Algebraic topology
Fractals
Number theory
Group theory
Homotopy theory
Queueing theory
Topology
Differential equations
Graph theory
Calculus
Fourier transform
Wolfram Alpha
Automatic differentiation
Game theory
Linear Programming
Computer Science
Programming
Programming languages
Data Science
Open Source
Languages
Text editors
Operating systems
Package managers
DevOps
Mindfulness
Compilers
Physics
Biology
Automation
Education
Economy
Governance
Consciousness
Drugs
Chemistry
Unix
Web
Cloud computing
Front End
Security
Social networks
Networking
Health
Fitness
Medicine
History
Travel
Geography
Business
Relationships
3D Printing
Anki
Philosophy
Video
Machine learning
Computer graphics
Tools
Design
Keyboards
Future
Cryptocurrencies
Privacy
Games
Streaming
Talks
Analytics
Databases
Art
API
Distributed systems
Backups
Space
Psychology
Sleep
IRC
Work
Management
LaTeX
Robots
NLP
Virtual Reality
Augmented Reality
Neuroscience
CLI
Humans
Philanthropy
Animals
Podcasts
Documentaries
Movies
TV series
Courses
Articles
Poems
Research papers
Books
Other
Notes
Code
Looking back
Powered By
GitBook
Automated theorem proving
β
Lean
is
great
.
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)
β
Previous
Satisfiability modulo theories
Next
Lean
Last modified
2mo ago
Copy link
Contents
Links