Institute for Computer-Aided Reasoning in Mathematics

The Institute for Computer-Aided Reasoning in Mathematics (ICARM) is a research institute at Carnegie Mellon University. It is funded by the U.S. National Science Foundation.

Leadership

Members include:

Palomar registry

Palomar is a registry of Lean verified mathematics, incubated by ICARM and the Lean FRO. Palomar's board includes some ICARM staff, as well as Bryna Kra, Terence Tao, Ravi Vakil, and Akshay Venkatesh. Kra noted in October 2026 that OpenAI had been encouraged to use Palomar, without success.

References

External links

This article about a mathematics organization is a stub. You can help Wikipedia by adding missing information.

[1] ttps://www.cmu.edu/news/stories/archives/2025/august/new-nsf-institute-at-cmu-will-help-mathematicians-harness-ai-and-advance-discoveries

[2] ttps://www.nsf.gov/news/nsf-invests-over-74-million-6-mathematical-sciences-research

[3] ttps://icarm.io/about/

[4] ttps://icarm.io/people/

[5] ttps://www.quantamagazine.org/the-ai-revolution-in-math-has-arrived-20260413/

[6] ttps://www.quantamagazine.org/to-have-machines-make-math-proofs-turn-them-into-a-puzzle-20251110/

[7] ttps://www.edtechinnovationhub.com/news/nsf-backs-new-carnegie-mellon-institute-to-apply-ai-in-mathematical-research-and-problem-solving

[8] ttps://icarm.io/news/announcing-palomar-a-registry-of-lean-verified-mathematics/

[9] ttps://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/

[10] ttps://palomar-registry.org/about#who-we-are

[11] ttps://www.wired.com/story/openai-is-pissing-off-a-bunch-of-mathematicians-again/

Institute for Computer-Aided Reasoning in Mathematics

Leadership

Palomar registry

References

Further reading

External links