What we are building

OpenMath is a developing platform for finding mathematical questions and understanding the work around them. Its long-term direction connects precise statements, literature, formalizations, attempts, results and useful next tasks, with provenance preserved throughout.

The current pilot offers a selected cross-field catalog and one maintained elementary-number-theory journey. A catalog entry can be useful before it has a Task or a formal proof; it must still disclose its source, scope and missingness.

Problems and Claims

A Problem is a canonical mathematical question, whether open or answered. Equivalent formulations share that record. A Claim is a precise proposition with assumptions, cited evidence and an explicit relation to its Problem: a formulation, supporting lemma, special case, conditional result, counterexample or bound.

Who maintains it

OpenMath is developed and operated by Akshay Painjane. Pilot publications and collection decisions are maintained by OpenMath staff. Independent expert assessment, contributor workflows and public execution have not been established for this pilot.

Backend and research contracts · Reader interface

What a status means

A source report is a dated assertion attributed to an identifiable source. An OpenMath decision records a named staff judgment within a collection and an explicit review scope. A passing Lean check records an exact machine outcome. None of these automatically supplies the other.

“Proved · full statement” concerns the whole question. A proved special case or conditional result leaves the general case open and names its remaining scope. Partial-progress coverage is stated explicitly when it has not been curated. A known theorem remains known when used as a formalization exercise. A staff repeat remains a repeat; independent reproduction and mathematical review need their own evidence.

Read the selection and checking method →

Corrections and attribution

Publications preserve their earlier versions when corrected. Source updates create candidates for staff review before they become visible. Rights are assessed per source; the external pilot uses source links and OpenMath paraphrases without mirroring full text.

How to report a correction →