The Proof Engine Programme: Reliable AI-Assisted Mathematics and Accountable Research

AI-assisted mathematics creates an opportunity to organize research around two interacting, potentially overlapping roles. Reliable mathematical production turns questions into warranted, readable results. Structural research extracts general mechanisms, connects results, develops new questions and creates tools. We argue that this division can help an expanding supply of mathematical arguments become shared mathematical knowledge. Human intelligence remains central to research design, structural judgment and responsible evaluation, while AI can contribute to both roles. In the Proof Engine programme, the author's primary expertise is engineering reliable production. He also contributes to structural development within his mathematical understanding, while looking to specialist mathematicians for deeper synthesis. Open problems supply inspiration and concrete tests; each investigation is directed toward a reusable mathematical contribution. Human authorship identifies this intellectual contribution and responsibility for the particular solution, its evidence and its correction. The programme tests this arrangement by connecting original questions, readable papers and inspectable formal evidence. Its completed formalization standard is kernel-only closure: the proof-assistant kernel checks the principal conclusions and their mathematical dependencies under declared foundations, while a separate review checks agreement with the intended mathematics. The immediate engineering challenge is to make these checks feasible; further work concerns reuse, structural understanding and research direction. We specify release commitments and prospective tests through which this account can be assessed.

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-09-08
DOI
https://doi.org/10.5281/zenodo.22653132
Primary Topic
Mathematics, Computing, and Information Processing
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

The Proof Engine Programme: Reliable AI-Assisted Mathematics and Accountable Research

Alex Chengyu Li
Zenodo (CERN European Organization for Nuclear Research)
Mathematics, Computing, and Information Processing
preprint

The Proof Engine Programme: Reliable AI-Assisted Mathematics and Accountable Research

Alex Chengyu Li
preprint en

Abstract

AI-assisted mathematics creates an opportunity to organize research around two interacting, potentially overlapping roles. Reliable mathematical production turns questions into warranted, readable results. Structural research extracts general mechanisms, connects results, develops new questions and creates tools. We argue that this division can help an expanding supply of mathematical arguments become shared mathematical knowledge. Human intelligence remains central to research design, structural judgment and responsible evaluation, while AI can contribute to both roles. In the Proof Engine programme, the author's primary expertise is engineering reliable production. He also contributes to structural development within his mathematical understanding, while looking to specialist mathematicians for deeper synthesis. Open problems supply inspiration and concrete tests; each investigation is directed toward a reusable mathematical contribution. Human authorship identifies this intellectual contribution and responsibility for the particular solution, its evidence and its correction. The programme tests this arrangement by connecting original questions, readable papers and inspectable formal evidence. Its completed formalization standard is kernel-only closure: the proof-assistant kernel checks the principal conclusions and their mathematical dependencies under declared foundations, while a separate review checks agreement with the intended mathematics. The immediate engineering challenge is to make these checks feasible; further work concerns reuse, structural understanding and research direction. We specify release commitments and prospective tests through which this account can be assessed.

Zenodo (CERN European Organization for Nuclear Research)
Mathematics, Computing, and Information Processing
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.