New Grant Supports Iron Man-Like Research

A Siena mathematics professor has received a prestigious grant to support his continuing work on the mathematics of quantum mechanics.

Jon Bannon, Ph.D. has been awarded the American Mathematical Society-Simons Research Enhancement Grant for Faculty at Primarily Undergraduate Institutions (PUIs). In addition to supporting the quantum mechanics work, the three-year grant in the amount of $3,000 annually will help fund study to formalize the foundations of the theory in the Lean 4 programming language.

The latter project is particularly exciting for Siena students, who will continue to have opportunities to work with Bannon and his collaborators on the Mathlib project to develop a verified formal mathematical library for use in AI-assisted mathematics research.

"ChatGPT is really good at spitting out convincing but untrustworthy arguments," explained Bannon. "One aspect of the library of verified mathematics we are building together with the mathematical community is that can eventually be used to teach an LLM [large language model] how well it is doing and to make sure the math it generates is correct."

Tossing in an "Iron Man 2" reference, he said the hope is that mathematicians will be able to collaborate with AI to make new discoveries in a way that will "look something like Tony Stark talking with Jarvis." (Welcome home, sir.)

This "Correspondences of von Neumann Algebras" grant will also help bring expert visitors to campus to support this project, and will support travel for collaborative research. Bannon works with fellow researchers at Vassar College and IIT Madras, among others, and the funds will facilitate future publication efforts.

"Using verified reasoning together with AI, we may eventually accelerate progress on scientific problems of human interest, such as renewable energy and disease research," he said.

Samyak Tuladhar '26 shared that since mathematics-and academia more broadly-thrives on open exploration and the free exchange of new discoveries, this path "avoids the ethical challenges often seen in creative fields.

"Through my many conversations with Dr. Bannon, I've come to truly value his wisdom and thoughtful perspective. We both share the belief that one of the most meaningful applications of AI is as a theorem-proving assistant," said Tuldhar. "I feel inspired by Dr. Bannon's vision, and I believe research like this holds great promise to benefit all of us."

Jack Cheverton '26 has academic interests in both computer science and mathematics, and is looking forward to seeing how formalizing the latter will impact the field.

"I'm especially excited about the possibilities of an AI being able to read and write Lean code. This could completely change how mathematicians solve problems.