Proof Engine 2.0：証拠に基づいて統括する自律的数学研究の方法

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.