Cited in
(38)- Vampire with a brain is a good ITP hammer
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- A neurally-guided, parallel theorem prover
- A Machine Learning Based Software Pipeline to Pick the Variable Ordering for Algorithms with Polynomial Inputs
- Improving stateful premise selection with transformers
- Improving ENIGMA-style clause selection while learning from history
- The role of entropy in guiding a connection prover
- Machine learning guidance for connection tableaux
- Deepalgebra -- an outline of a program
- MPTP 0.2
- ML4PG
- MaLeCoP
- MaSh
- FEMaLeCoP
- SEPIA
- kFOIL
- Theoryguru
- OpenNMT
- ATPboost
- ENIGMA
- Proofwatch
- TacticToe
- Holophrasm
- MachSMT
- Machine learning for mathematical software
- The role of the Mizar mathematical library for interactive proof development in Mizar
- nFOIL
- mizar-items
- lazyCoP
- MedleySolver
- A plugin to export Coq libraries to XML
- Hammer for Coq: automation for dependent type theory
- NeuroSAT
- ProofWatch: watchlist guidance for large theories in E
- IMLI
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- HOList
- GamePad
This page was built for software: DeepMath
