Dictionary
Concept dictionary
The vocabulary you need to read this archive. Each entry is the term as the field uses it, paired with a paper in the corpus where Urban works with it.
The definitions are ours, written to get you into the papers — they are not quotations of Urban. The citation under each one is the part that is his.
- Automated theorem prover (ATP)
- A program that searches for a proof of a conjecture from a set of axioms with no human in the loop — it either finds one, runs out of time, or reports failure. Powerful in principle and combinatorially explosive in practice, which is the gap most of this archive works in.
- In the corpus Learning Guided Automated Reasoning: A Brief Survey (2024) ↗
- Proof assistant (ITP)
- The interactive counterpart: a system in which a human writes a proof and the machine checks every step. Mizar, HOL Light, HOL4, Isabelle and Coq all appear in this corpus — a hammer is the bridge from one of these to an ATP.
- In the corpus Mizar: State-of-the-art and Beyond (2015) ↗
- Mizar Mathematical Library (MML)
- One of the largest bodies of formalized, machine-checked mathematics, written in the Mizar language over decades. It is the substrate for much of this archive: first as something to translate, later as a training set.
- In the corpus Translating Mizar for First Order Theorem Provers (2003) ↗
- MPTP
- Mizar Problems for Theorem Proving — Urban’s translation of the Mizar library into first-order problems that ordinary automated provers can attempt. The move that turns a library of human proofs into a benchmark and a training corpus.
- In the corpus MPTP 0.2: Design, Implementation, and Initial Experiments (2006) ↗
- Premise selection
- Choosing which of thousands of available facts to hand a prover for a given conjecture. Called out in this corpus as “one of the main bottlenecks in the formalization of mathematics” — get it wrong and a solvable goal becomes unreachable.
- In the corpus DeepMath - Deep Sequence Models for Premise Selection (2016) ↗
- Large-theory reasoning
- Automated reasoning in settings where thousands of theorems, definitions and lemmas are available at once and consistently reused, rather than the handful of axioms a classical prover expects. The setting MaLARea was built for.
- In the corpus MaLARea: a Metasystem for Automated Reasoning in Large Theories. (2007) ↗
- Hammer
- A tool inside a proof assistant that takes the current goal, selects relevant facts, ships the problem to external automated provers, and reconstructs any proof that comes back as a checked proof in the assistant. The user experience of everything above.
- In the corpus HOL(y)Hammer: Online ATP Service for HOL Light (2014) ↗
- Clause selection
- Inside a saturation-style prover, the repeated choice of which clause to process next — the single most consequential decision in the search loop, and the one ENIGMA learns to make from previous proofs.
- In the corpus ENIGMA: Efficient Learning-Based Inference Guiding Machine (2017) ↗
- Tactic
- A proof-assistant command that transforms a goal into subgoals — the unit a human actually writes. TacticToe learns, from human proofs, which tactic suits a situation, and searches at that level rather than over raw inference steps.
- In the corpus TacticToe: Learning to Prove with Tactics (2020) ↗
- Property-invariant embedding
- A way of representing logical formulas for a neural network so that the representation does not depend on the particular names of symbols — so a learner generalizes across problems that use different vocabulary for the same structure.
- In the corpus Property Invariant Embedding for Automated Reasoning (2020) ↗
- Conjecturing
- Producing the statement to be proved rather than the proof of a given statement — here, learning to invent the induction predicates that hard arithmetic problems need, starting from no examples of them.
- In the corpus Learning Conjecturing from Scratch (2025) ↗
- Autoformalization
- Translating ordinary mathematical prose into a formal language a proof assistant can check — the reverse direction from MPTP. In this corpus it moves from a neural-machine-translation experiment on Mizar to a textbook of topology formalized at scale.
- In the corpus Exploration of neural machine translation in autoformalization of mathematics in Mizar (2020) ↗