Start with a step that can be checked
You can publish complete research, special cases, constructions, computations or failed attempts. Authors who want to take part in the formalization activity can upload Lean files for a specific version and choose the declarations to check. Not taking part, a failed check or having no formal proof yet never affects publication.
This activity is run independently by Eksmu. The public problems and tools of the Justin Sun Mathematics Prize serve as a reference; this site has no confirmed partnership with the organizer, and our reports are not official acceptance or an award.
How to take part now
- Publish material you have the right to make public in the research workspace, keeping a fixed version and the attachments you choose.
- In that version’s “Opt in to a private Lean pre-check” panel, choose the .lean attachment, target declaration and problem source, and explicitly authorize a local check.
- A maintainer runs a restricted, offline single-file check. The author receives a report stating what was checked, the tool version, the result and what was not checked.
- The author revises their materials based on the report and decides for themselves whether to submit, under the prize organizer’s current rules.
On the public site, every attachment uploaded to a research version can be read by readers, including the original .lean files. What stays private is the enrollment and the check report, not the uploaded source. Pre-checks are currently started manually by a maintainer with no turnaround guarantee; they are not full project verification with external dependencies, and nothing — papers, code or enrollment — is sent to the organizer automatically.
Three separate questions when reading a report
- Did the tool actually run, and did the selected declaration pass the mechanical check?
- Does the declaration faithfully state the original problem, with hypotheses and conclusion covering the claimed result?
- Does it meet the organizer’s independent review, publication and claim requirements?
Success on the first does not imply the other two. Finite computations, special cases and demo files should state their scope clearly.
External rules are set by the prize’s official website and official public repository. Where official pages differ, confirm with the organizer before any formal submission.