Mathematics

Responsible: Ben Goertzel (architecture)

Papers: Hyperon for AGI⇒ASI Whitepaper (2025), §9.4

GitHub: chaining (forward/backward chaining, proof synthesis), mm2metta (Metamath→MeTTa converter), mmverify.py (Metamath verifier)

Status: Existing tools include MeTTa forward/backward chaining (chaining repo), Metamath-to-MeTTa conversion (mm2metta), and a Metamath proof verifier (mmverify.py). The whitepaper reports an MM2 proof verifier implemented inside MORK as a fast graph-local proof kernel. The broader automated conjecturing pipeline described below is the proposed research direction.

Most automated theorem proving focuses on proving stated goals, but mathematicians spend much of their time on conjectures — formulating new definitions, lemmas, and "what if" hypotheses that later get proved, refuted, or refined. Hyperon targets automated conjecturing as the primary goal, then uses formal proof for validation.

Proposed Architecture (from Whitepaper)

The whitepaper describes a pipeline built around the MORK/MM2 proof verifier kernel:

• Knowledge base: Definitions, theorems, proofs, and proof tactics stored as Atoms. A MathSpace wrapper would handle import/export to external proof assistants while maintaining CIDs and equivalence classes internally.
• Pattern discovery: Pattern Miner finds proof motifs (induction schemas, commutativity tricks) ranked by surprisingness. WILLIAM promotes frequent motifs to templates for tactic prediction and proof search heuristics.
• Conjecture engine: Conjecturing framed as geodesic search over typed expressions — forward factors from known lemmas, backward factors from gaps to close, weakness bias toward simple statements, TransWeave reuse of isomorphic substructures from neighboring theories.
• Proof verification: Candidate conjectures enter a pipeline — schematic proofs with PLN hints, external provers when helpful, then validation in the MM2 proof verifier on MORK.

Current Tools

• chaining — MeTTa implementations for automated reasoning: forward/backward chaining, program synthesis, PLN integration, Metamath reasoning, and modal logic experiments
• mm2metta — Converts Metamath formal proofs (.mm) to MeTTa (.metta) format, bridging formal verification with Hyperon's symbolic reasoning
• mmverify.py — Pure Python Metamath proof verifier (~700 lines), providing an independent verification baseline

Key References

• Goertzel, B. (2025). Hyperon for AGI⇒ASI Whitepaper, §9.4: Mathematical Theorem Proving with Automated Conjecturing