Proof Engine 2.0: An Evidence-Governed Method for Autonomous Mathematical Research

Artificial intelligence can assist mathematical research by generating arguments, checking proofs expressed in a formal language, and exploring possible questions. Autonomous research also requires a reliable account of how these activities contribute to an investigation. My earlier Proof Engine Infrastructure, called 1.0 here, addressed the composition of mathematical evidence: it attached each assertion to its exact statement, supporting evidence and dependencies, and reconsidered dependent results after correction. This supplied a persistent basis for proof development. A further problem arises when agents select and revise the research question itself. A valid proof can concern a known result, answer a different request, or leave the broader mathematical objective unresolved. Proof Engine 2.0 adds a project-level method for managing that changing objective. It connects source and existing-solution inquiry, correspondence between the intended and proved statements, and deductive closure by recording the question, intended result and required evidence. A local implementation combines a versioned library of agent procedures, persistent research records, scope-preserving mathematical returns and mechanical record checks. Agents consult a retained set of investigated questions, identify tractable attack points and submit proposals for human approval. Six completed-result cases and a developmental tropical case trace mathematical development through author–agent interaction. Human structural judgments in the benzel, canon-permutation and tropical investigations redirect autonomous work toward broader results. These investigations also led to changes in the procedures for selecting and assessing further research. Autonomous execution takes place within human-approved research scope. The implemented method preserves 1.0 as a proof-development component. Comparative performance and independent transfer remain questions for prospective evaluation.

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-09-05
DOI
https://doi.org/10.5281/zenodo.22346064
Primary Topic
Logic, programming, and type systems
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

Proof Engine 2.0: An Evidence-Governed Method for Autonomous Mathematical Research

Alex Chengyu Li
Zenodo (CERN European Organization for Nuclear Research)
Logic, programming, and type systems
preprint

Proof Engine 2.0: An Evidence-Governed Method for Autonomous Mathematical Research

Alex Chengyu Li
preprint en

Abstract

Artificial intelligence can assist mathematical research by generating arguments, checking proofs expressed in a formal language, and exploring possible questions. Autonomous research also requires a reliable account of how these activities contribute to an investigation. My earlier Proof Engine Infrastructure, called 1.0 here, addressed the composition of mathematical evidence: it attached each assertion to its exact statement, supporting evidence and dependencies, and reconsidered dependent results after correction. This supplied a persistent basis for proof development. A further problem arises when agents select and revise the research question itself. A valid proof can concern a known result, answer a different request, or leave the broader mathematical objective unresolved. Proof Engine 2.0 adds a project-level method for managing that changing objective. It connects source and existing-solution inquiry, correspondence between the intended and proved statements, and deductive closure by recording the question, intended result and required evidence. A local implementation combines a versioned library of agent procedures, persistent research records, scope-preserving mathematical returns and mechanical record checks. Agents consult a retained set of investigated questions, identify tractable attack points and submit proposals for human approval. Six completed-result cases and a developmental tropical case trace mathematical development through author–agent interaction. Human structural judgments in the benzel, canon-permutation and tropical investigations redirect autonomous work toward broader results. These investigations also led to changes in the procedures for selecting and assessing further research. Autonomous execution takes place within human-approved research scope. The implemented method preserves 1.0 as a proof-development component. Comparative performance and independent transfer remain questions for prospective evaluation.

Zenodo (CERN European Organization for Nuclear Research)
Industry, innovation and infrastructure
Logic, programming, and type systems
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.