UF team receives $814,000 to bring AI proof feedback to advanced math courses

A University of Florida-led team has received an $814,000 grant to bring an AI proof-feedback tool into advanced undergraduate mathematics. The project will extend HaLLMos beyond introductory proof courses into linear algebra, real analysis and topology, while preserving its central design: helping students spot weaknesses in their reasoning without handing them complete solutions.

Written rules for feedback, not answers

Led by UF mathematics professor Vincent Vatter, the team designed HaLLMos to respond to students’ written proofs. Its role is to identify weaknesses and help students work toward corrections themselves. That makes the feedback a step in the student’s work, rather than a replacement for completing it.

The tool uses what the university calls constitutional AI: a written set of principles guides how the system responds. Mathematicians and mathematics educators developed those principles with two goals—feedback that is mathematically sound and guidance that is useful for learning. Those are the project’s design aims, not a guarantee of every response.

The educational idea is “productive struggle”: engaging with difficult but achievable problems to build understanding and independent problem-solving skills. HaLLMos is intended to preserve that process while providing targeted help. Vatter argues that removing the difficulty altogether also removes part of what students need to learn.

Advanced subjects need their own examples

The award comes from the AI for Math Fund, supported by Renaissance Philanthropy and XTX Markets. It will pay for the expansion into the three advanced subjects and support a fellowship program involving approximately 40 mathematicians. The planned fellows include faculty members, postdoctoral researchers and graduate students from institutions across the country.

The research team also includes Sarah Sword, principal research scientist at Education Development Center; Jay Pantone, an associate professor of mathematics at Marquette University; and Ryota Matsuura, a mathematics professor at St. Olaf College. The project builds on earlier work supported by the National Science Foundation.

A revision loop before the grade

HaLLMos already has a base of classroom use: nearly 40,000 student proofs have been submitted, according to the university. Vatter describes an instructional capacity problem behind the project. Students learning to write proofs need substantial individualized feedback, he says, and instructors do not have enough capacity to provide all of it.

Vatter has incorporated the tool into his own teaching so students can test proofs before submitting assignments. They can submit a proof, receive feedback, revise it and submit again. His stated goal is to let students learn through that revision process instead of encountering only a grade at the end.

The existing tool is freely available to students and instructors at hallmos.com. Students can practice writing proofs and receive immediate feedback, while instructors can create exercises for their courses. The grant supports taking that approach into advanced undergraduate subjects; it is not the tool’s first public release.