ICARM mentioned in Quanta
ICARM director Jeremy Avigad is quoted in Quanta Magazine's survey of AI's arrival in mathematical research.
Quanta Magazine's April 2026 feature The AI Revolution in Math Has Arrived, by Konstantin Kakaes, surveys how artificial intelligence has moved from solving competition problems to helping mathematicians discover and verify genuinely new results — and ICARM director Jeremy Avigad is among the researchers it quotes.
"One reason there is so much interest in AI for mathematics in the corporate world is that people are recognizing that the key to general intelligence is combining the insights you get from machine learning and the precision you get from mathematics."
That pairing — the pattern-finding of machine learning with the guarantees of machine-checked proof — is exactly what ICARM was founded to study. The article traces a fast year: in July 2025, AI systems solved five of six International Mathematical Olympiad problems; by February 2026, the "First Proof" challenge showed AI handling more than half of ten research-level problems with minimal human help. As these systems generate more mathematics, Quanta argues, formal verification becomes essential to separate reliable results from plausible-looking error — what the article calls "autoformalization."
Read the full article at Quanta Magazine.