New AI Tool HaLLMos Helps Students Learn the Art of Writing Mathematical Proofs

Mathematics students often reach a turning point in their studies when they encounter proofs for the first time. Solving equations, calculating probabilities, or working with matrices usually feels concrete and procedural. Proofs, on the other hand, demand something very different: logical structure, creativity, and the ability to explain why something is true rather than just showing that it works. This transition is where many students struggle, and it is exactly the gap a new AI-powered tool called HaLLMos is designed to address.

HaLLMos is an educational tool developed to support students as they learn how to write mathematical proofs. Rather than replacing instructors or handing students complete solutions, the tool focuses on guiding students through the reasoning process, offering feedback that helps them refine their ideas and strengthen their arguments. The goal is to make proofs feel less intimidating and more approachable, while still preserving the intellectual challenge that makes them valuable.

Why Proofs Are So Hard for Students

For many students, proofs are their first encounter with open-ended mathematical thinking. In computational problems, there is typically a single correct answer and a well-defined method for reaching it. Proofs, by contrast, can be approached in multiple valid ways. Two students might solve the same problem using entirely different arguments, and both proofs could be correct.

This openness often confuses students. They may feel unsure whether their reasoning is sound, even if they are on the right track. Feedback from instructors is essential at this stage, but providing detailed, individualized feedback takes time—something many faculty members simply do not have enough of, especially in large classes.

HaLLMos was created to help fill this gap by offering immediate, personalized feedback while students are still in the process of constructing their proofs.

Who Built HaLLMos and How

The project is led by Professor Vincent Vatter, a mathematician in the University of Florida’s Department of Mathematics. He serves as the principal investigator for the project and introduced the tool directly into his teaching, including in his “Reasoning and Proof in Mathematics” course, a required class for math majors that is often students’ first formal exposure to proofs.

Vatter worked alongside a multidisciplinary team that combines expertise in mathematics, mathematics education, and computer science. The collaborators include 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 Matsuura, a professor of mathematics, statistics, and computer science at St. Olaf College.

The development of HaLLMos was supported by funding from the National Science Foundation, reflecting a broader interest in improving undergraduate STEM education through thoughtful uses of artificial intelligence.

How HaLLMos Works in Practice

At its core, HaLLMos is powered by a large language model, but it has been carefully designed to behave very differently from generic AI chatbots. The team’s guiding principle was that the tool should support learning, not short-circuit it.

When a student submits a proof attempt, HaLLMos does not provide a full solution. Instead, it analyzes the structure and logic of the argument and responds with feedback that points out gaps, unclear steps, or logical issues. The feedback encourages students to rethink specific parts of their proof and try again, much like a professor might do during office hours.

Students can choose from a set of classic proof exercises, such as demonstrating that if the square of an integer is even, then the integer itself must also be even. These are standard problems in early proof-based courses and serve as ideal practice examples. HaLLMos also offers a sandbox mode, where students can enter problems from any course and receive feedback on their own custom proofs.

Faculty members can go a step further by creating exercises within the system and sharing them directly with their students. This makes HaLLMos adaptable to different courses and teaching styles, rather than being limited to a fixed set of problems.

A Tool Inspired by Mathematical Creativity

The name HaLLMos is a tribute to the late mathematician Paul Halmos, who famously argued that mathematics is a creative art, much like painting or music. This philosophy is deeply embedded in the design of the tool. Proofs are not treated as rigid templates to be memorized, but as creative constructions that students learn by experimenting, failing, revising, and improving.

By offering feedback in real time, HaLLMos allows students to engage more deeply with this creative process. They can test ideas, see where their reasoning breaks down, and adjust their approach without having to wait days or weeks for graded feedback.

Benefits for Both Students and Professors

From the student perspective, HaLLMos provides a low-pressure environment to practice proofs. Students can explore ideas freely, knowing they will receive guidance rather than judgment. This can be especially helpful for those who feel anxious about proofs or worry that they are “not good at math.”

For professors, the tool helps address a long-standing challenge: the lack of time for individualized feedback. While HaLLMos is not meant to replace human instruction, it can handle some of the routine feedback that instructors would otherwise struggle to provide at scale. This allows faculty to focus their time on deeper discussions, conceptual questions, and mentoring.

Future Plans for HaLLMos

The development team sees HaLLMos as an evolving project rather than a finished product. One major goal is to expand its use beyond a single institution by recruiting additional pilot sites. Testing the tool in different classroom contexts will help refine its feedback and ensure it works well across a wide range of undergraduate mathematics courses.

Another long-term aim is to make HaLLMos effective for any type of undergraduate proof, not just the introductory examples. This includes proofs in areas such as abstract algebra, real analysis, and combinatorics, where reasoning becomes more complex and nuanced.

There are also plans to explore hosting the tool on HiPerGator, the University of Florida’s high-performance computing system. Doing so could improve scalability and performance while keeping the tool freely accessible to the public, which remains a central commitment of the project.

AI and the Future of Mathematics Education

HaLLMos is part of a growing movement to use AI thoughtfully in education. Unlike tools that simply generate answers, educational AI systems like this one aim to model good teaching practices. In mathematics, this is especially important, because understanding how to think is far more valuable than memorizing results.

Proof-based learning sits at the heart of mathematical thinking. It teaches students to reason carefully, communicate clearly, and build arguments that stand up to scrutiny. Tools like HaLLMos suggest that AI, when designed with care, can support these goals rather than undermine them.

As AI continues to find its place in classrooms, HaLLMos offers a compelling example of how technology can be used to enhance learning without replacing human insight. By helping students navigate the challenging but rewarding world of proofs, it opens the door for more learners to engage deeply with mathematics as a creative and logical discipline.

Research reference:
https://www.edc.org/projects/artificial-intelligence-for-humanizing-and-enhancing-the-learning-of-proofs