What “Exact” means
“Exact” describes our commitment to explicit statements, traceable reasoning, and transparent verification—not a claim that every preliminary result is already correct.
An independent research initiative exploring mathematics with AI. We share preliminary results, develop reusable formal mathematics, and build explanations that help readers understand proofs. Each project records its verification status and how that status changes over time.
Why this initiative exists
The work starts from a practical difficulty: producing a proof and coming to understand it are different tasks. A growing body of AI-assisted mathematics should not become a collection of opaque results.
We want to retain precise claims, reusable formal tools, and explanations that let a reader follow the necessary mathematics without reconstructing every missing link from external literature.
AI participation and human responsibility
AI may contribute to exploration, proof construction, formalization, literature searches, and exposition. The role of AI and the extent of human review should be recorded for each result rather than hidden behind a general label.
A preliminary briefing is not a peer-reviewed article. Later papers record their actual human contributions; a preliminary website record does not predetermine their authorship.
Versions, corrections, and unfinished work
A project is a changing record, not a permanent claim of correctness. Substantive corrections should identify the affected statement and version. A known error should be marked as an error, not left under an ambiguous “unverified” label.
Formal checking and ordinary mathematical writing can proceed in either order. We aim to bring both to completion, while making each useful intermediate result available under an accurate description of its state.
Brief reports are independent records
Brief reports retain mathematical statements, proofs, necessary notation, and references without waiting for a conventional paper. The standard label is “AI-assisted manuscript”; the human-verification notice describes the report version.
Lean, MathlibAnnex, explanatory-material, and publication milestones are recorded on project pages. A later milestone does not by itself require the report PDF to be revised.
Brief reports are distributed as PDFs. Editable manuscript sources are retained privately and may be shared individually by agreement. This does not determine the separate release policy for Lean code or MathlibAnnex.
Operator
Ryotaro Tanaka
Associate Professor
Institute of Arts and Sciences
Tokyo University of Science
The affiliation is provided for identification only. Exact Mathematics with AI is an independent research initiative and is not an official website or publication of Tokyo University of Science.
Institutional profile — identification
Corrections and prior-art feedback
Use the corrections form for substantive corrections, prior-art feedback, and website enquiries.