Oct 12, 2026
Webinar: First Proof, Third Batch Results
Ten research-level problems, solutions from several AI systems, refereed blind by experts. Wednesday, October 14 at 3:00 PM ET, with live Q&A.
Institute for Computer-Aided Reasoning in Mathematics
ICARM supports the use of new technologies for computer-aided reasoning and discovery in mathematics. The institute is hosted by Carnegie Mellon University on its campus in Pittsburgh.
- Formal methods and proof assistants
- Automated reasoning and symbolic AI
- Machine learning and neural AI
Robert Mehrabian Collaborative Innovation Center · CMU
News
Aug 21, 2026
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.
Aug 20, 2026
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/
Upcoming events
Oct
29
Modern Math Workshop at the SACNAS Annual Conference
Other · October 29, 2026 · Long Beach, CA
→
Nov
4
Formalization for Physics
Workshop · November 4 – 6, 2026 · Pittsburgh, PA
→
Jan
13
JMM 2027 Tutorial - Lean, AI, and the Future of Mathematical Proof: A Hands-On Tutorial from ICARM
Tutorial · January 13 – 14, 2027 · Chicago, IL
→