Primary evidence
- MaLARea: a Metasystem for Automated Reasoning in Large TheoriesS1 · Primary research · Paper · 2007-06-27
MaLARea closes a machine-learning and theorem-proving feedback loop over large theories
The system repeatedly trains relevance models from existing proofs, invokes automated provers on selected premises and incorporates newly found proofs into subsequent learning rounds.
What happened?
Josef Urban's MaLARea paper was published with the ESARLT 2007 workshop proceedings on 27 June 2007 and described a metasystem combining machine learning, automated theorem proving and model finding for large theories.
Why it matters
The deduction–learning feedback loop became a core pattern for later self-improving theorem-proving systems and anticipated modern search-and-learning agents for formal mathematics.
Significance rationale: MaLARea made large-theory reasoning explicitly iterative: machine learning selects useful knowledge, ATP systems attempt proofs, and successful results are fed back into the learner for subsequent problems.
Historical context
Earlier developments
—
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Autonomous primary role
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Learned premise-selection models and automated provers interacted in an autonomous loop that improved from previous proof results.
- Human contribution
- Josef Urban designed the metasystem, learning/reasoning loop, data interfaces and experiments.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- malarea
- Organizations
- charles-university
- Problems
- large-theory-theorem-proving
- Methods
- machine-learning, premise-selection, automated-theorem-proving, model-finding, feedback-loop
Sources & artifacts
- MaLARea: a Metasystem for Automated Reasoning in Large TheoriesS1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 2007-06-27 · Paper released · E2 · Research record
The CEUR proceedings establish the MaLARea system and its learning/reasoning architecture.
Corrections
No corrections recorded.