OpenMath · research in context
A shared record of mathematical work.
Trace a claim to its source, understand the prior work, and inspect exactly what a result establishes. This reference example follows one known theorem through a concrete task and two local Lean runs.
A connected example
Begin with a known theorem, then follow the claim, the next piece of work, and its recorded outcome.
Problem · elementary number theory
Why are there infinitely many primes?
The source note, related formal statements, and proof idea are linked in one place.
Known theoremFollow-up task
Formalize a prime strictly above every bound
A bounded Lean exercise. A sample solution and its failed predecessor are both recorded.
View task and context →Follow the work
01 · Understand
Source and claims
Read the cited wording and see how related formal statements are linked.
Inspect a claim →02 · Continue
Task and context
Start from a pinned set of sources, proof ideas, and the known failed route.
Open starting context →03 · Assess
Runs and review
Compare the Lean outcomes with source alignment and human review shown separately.
Inspect the passing run →