New AI-powered tool helps students find creative solutions to complex math proofs
Math students may not blink at calculating probabilities, measuring the area beneath curves or evaluating matrices, yet they often find themselves at sea when first confronted with writing proofs.
But a new AI-powered tool called HaLLMos — developed by a team led by Professor Vincent Vatter, Ph.D., in the University of Florida Department of Mathematics — now offers a lifeline.
“Some students love proofs, but almost everyone struggles with them. The ones who love them just put in more work,” Vatter said. “It just kind of blows their minds that there’s no single correct answer — that there are many different ways to do this. It’s very different than just doing computational work.”
Building the tool
HaLLMos was developed by Vatter, as principal investigator, along with Sarah Sword, a mathematics education expert at the Education Development Center; Jay Pantone, an associate professor of mathematical and statistical sciences at Marquette University; and Ryota Matsurra, a professor of mathematics, statistics and computer science at St. Olaf College; with grant support from the National Science Foundation. The tool is freely available at hallmos.com.
The team’s goal was to develop an AI tool powered by a large language model that would support student learning rather than short-circuiting it. HaLLMos provides immediate personalized feedback that guides students through the creative struggle that writing proofs requires, without solving the proofs for them.
The tool’s name honors the late Paul Halmos, a renowned mathematician who argued that the mathematics field is a creative art, akin to how painters work.
Students using HaLLMos can select from classic exercises — such as proving that, for all integers, if the square of the integer is even, the integer is even — or use “sandbox mode” to enter exercises from any course. Faculty can create exercises and share them with students.
Vatter introduced HaLLMos to his students last spring in his “Reasoning and Proof in Mathematics” class, a core requirement for math majors that is often the first time students encounter proofs.
“They could use this tool to try out their proofs before they brought them to me. We try to identify the error in a student’s proof and let them go fix it,” Vatter said. “It is difficult for faculty to devote enough time to working individually with students. Our goal is that this tool will provide the feedback in real time to students in the way we would do it if we were there with them as they construct a proof.”
Helping professors and students excel
“I think every math professor would love to give more feedback to students than we are able to,” Vatter said. “That’s one of the things that inspired this.”
The next steps for Vatter and his colleagues include getting more pilot sites to use the tool and continuing to improve its responses.
“We’d like it to be good at any kind of undergraduate mathematics proofs,” he said.
Vatter also intends to explore moving HaLLMos to UF’s HiPerGator, the country's fastest university-owned supercomputer.
“It’s our goal to have it remain publicly accessible,” Vatter said.
This research was supported by a grant from the National Science Foundation Division of Undergraduate Education.