Development

A specialist system autoformalizes two number-theory papers

development2026-06-07

Claim

LeanMarathon autoformalizes research mathematics in Lean over hours-long runs, clearing every target in two number-theory papers, while Adaption Labs opened a $50,000 four-week challenge to release goal-adapted models openly.

Reported metric: $50,000 prize

Reporting date: 2026-06-07 (not necessarily the event date)

Sources

Attribution and reporting linked by this record; links do not imply independent verification.

Welcome to June 7, 2026 (theinnermostloop.substack.com)

Knowledge graphopen in browser →

Reported in

Welcome to June 7, 2026

Actor

Adaption Labs

Evidence for

Supersedes

Sixteen mathematicians publish a declaration on AI and mathematics

Referenced by

Cite or correct this record

Citation formatCitation text

A specialist system autoformalizes two number-theory papers
Innermost Loop KB — secondary record
Reporting date: 2026-06-07
KB permalink: https://nicholsn.github.io/innermost-loop-kb/developments/2026-06-07-a-specialist-clears-two-papers-in-lean
Claim: LeanMarathon autoformalizes research mathematics in Lean over hours-long runs, clearing every target in two number-theory papers, while Adaption Labs opened a $50,000 four-week challenge to release goal-adapted models openly.
Attributed sources:
- Welcome to June 7, 2026 — https://theinnermostloop.substack.com/p/welcome-to-june-7-2026
This citation does not imply independent verification of linked-source claims.

Suggest a correction — opens a GitHub draft for you to review and submit.