News
Announcing Palomar, a registry of Lean verified mathematics
Palomar, a public registry of Lean formalizations whose proofs have been machine-checked, is now open for submissions. Incubated by ICARM together with the Lean FRO, it gives formalized results a durable, citable record after three automated checks of the proof, the statement, and the submission's disclosures.
New record breaking elliptic curve reported
New record in arithmetic geometry: the first known elliptic curve with rank 30 was uploaded to ICARM's Elliptic Curve Rank Leaderboard, surpassing the rank-29 record set by Elkies & Klagsbrun in 2024. Details + discussion: https://icarm.io/news/new-record-breaking-elliptic-curve-reported/
The last sporadic group falls: Team realizes M23 as a Galois group over the rationals
Forty years after the other 25 sporadic groups were settled, an explicit degree-23 polynomial shows that M23 is a Galois group over Q.
ICARM endorses the Leiden Declaration
We endorse the Leiden Declaration as an important first step in helping the mathematics community grapple with the use of AI.
Milestones workshop frames AI progress in mathematics
ICARM and Principia Labs convened mathematicians and AI researchers in San Francisco to define meaningful milestones for autonomous mathematics research.
ICARM mentioned in Quanta
ICARM director Jeremy Avigad is quoted in Quanta Magazine's survey of AI's arrival in mathematical research.
FirstProof discussion finds a public home on ICARM Zulip
ICARM's public Zulip has become a working forum for mathematicians and AI researchers evaluating FirstProof claims, from Aletheia's results to Cursor, Archon, and other follow-on efforts.
Join ICARM at JMM 2026
Find ICARM at the 2026 Joint Mathematics Meetings in Washington, DC — at our exhibition booth and a two-part tutorial on automated reasoning.
NSF launches ICARM as a pilot institute
The National Science Foundation has established ICARM at Carnegie Mellon as one of six new mathematical sciences research institutes, part of a $74-million investment.