Math grad aims to specialize in computer verification of mathematical proofs

Editor’s note: This story is part of a series of profiles of notable fall 2022 graduates.

Sage Binder is the recipient of the prestigious Dean’s Medal for the School of Mathematical and Statistical Sciences in honor of his steadfast commitment to academic excellence. He will be recognized by The College of Liberal Arts and Sciences at Arizona State University during the fall 2022 convocation this week, where he will graduate with a bachelor’s degree in mathematics and a minor in philosophy.

Binder started his college career at Paradise Valley Community College, preparing to transfer into a software engineering degree at ASU. When he looked at the course list for the major, he did not find the courses very interesting. He decided to look at the mathematics degree pathway just to see what kind of courses were offered.

“Absolutely everything looked interesting to me. I wanted to take everything that was offered,” said Binder.

It took a while for him to feel comfortable about leaving the software engineering pathway, which he was initially so focused on, but by the time he entered ASU, he was committed to majoring in mathematics.

“I have had absolutely no regrets. I do still enjoy coding and computer science, however, and much of what I want to research in the future involves the intersection between mathematics, theoretical computer science and applied computer science.”

Binder was born and raised in Phoenix by parents who both have bachelor’s degrees in chemistry. His mother pursued a master’s degree in computational biosciences at ASU. His father went into industry, which took the family for a few years each to Anchorage, Alaska, and Cairo, Egypt, then back to Arizona in 2014. He was homeschooled for much of his childhood.

“I think being homeschooled definitely allowed me to explore mathematics in a way that a lot of other students don’t have the opportunity to do, which is unfortunate,” said Binder.

One of Binder’s favorite courses was Differential Geometry with President’s Professor Matthias Kawski.

“Sage was extremely well-read, always perfectly prepared with many questions and suggestions, and going substantially beyond each class' core content,” said Kawski. “He was an effective creator and leader of student teams, and always reaching out to all other peers, many of whom needed basic help.”

“It was a very fun class,” said Binder. “Professor Kawski lets students do a final presentation for a portion of the final exam grade, so I had a lot of fun putting a presentation together alongside two classmates. My work for the presentation eventually resulted in my research work with him over the summer of 2022.”

“Sage’s team produced an outstanding final project and presentation on parallel transport on curved spaces/surfaces,” said Kawski. “This led to his undergraduate summer research project on computing and interactively visualizing curvature flows, such as the Ricci flow, the mean curvature flow and others, and him making the new sympy code publicly available via GitHub.

“A special highlight is the reproduction of a notorious sequence of images visualizing the Ricci flow on two-dimensional surfaces of revolution (in general, it is impossible as the two-dimensional manifolds on which the Ricci flow evolves cannot be embedded into three-space). This work went far beyond symbolic computation and required Sage to invent special tools to resolve severe numerical issues at nasty singularities of the flow.”

The results of Binder’s summer project were to be presented as a major invited address at an international conference in Prague in early December, but had to be postponed due to professor Kawski’s recent medical issues.

Becoming part of ASU’s mathematical community has been a positive experience for Binder.

“I’ve met so many cool people and have had wonderful opportunities for collaboration with students and professors,” said Binder. “All of my professors have been great mentors in different ways. I have also learned a lot by talking to other students, and particularly other grad students, who helped me navigate the process of applying to graduate schools. I’ve had great conversations with students and professors at events such as Coffee Break. I should make special note of Dr. Zilin Jiang, our faculty advisor for the Mathematics Tomorrow Club. He has spent countless hours with us students during club meetings, talking about many aspects of research mathematics which aren’t usually discussed in class. I’ve learned a lot from interacting with him during our club meetings.”

Binder is an officer in Mathematics Tomorrow, a newly formed student club in the school. The club aims to create a community of students who enjoy solving mathematical problems in a variety of areas and want to strengthen their creative mathematical skills, as well as their skills at doing mathematical proofs.

“Sage is one of the most mathematically curious students in the club,” said Assistant Professor Zilin Jiang. “I think he genuinely appreciates the beauty of mathematical problem-solving — the difficulty of a problem is right in front of you, and you have to be creative to solve that problem.

“He is very drawn towards automated theorem proving. The idea here is to prove mathematical theorems by computer programs. A simpler, but related problem is automated proof verification. He hopes to further explore this area after graduation.”

Binder recently finished applying to graduate schools, which he hopes to start next fall. His intended research direction is to investigate the use of computer systems to verify mathematical theorems from the basic axioms of logic and set theory. He is further interested in the potential use of software to not only verify proofs, but also to actively assist in discovering proofs.

“Sage has an exceptionally well-thought plan for his PhD research and beyond, specializing in computer verification of mathematical proofs,” said Kawski. “This is an ever-more important critical issue in our modern world, which is run over by often unverified algorithms from so-called machine learning and artificial intelligence.”

We asked Binder to share more about his journey as an ASU Sun Devil.

Question: Why did you choose ASU?

Answer: I began my college career by taking classes at Paradise Valley Community College. Since the community college system has a smooth transfer pathway to ASU, it was a natural choice.

Q: What do you like most about mathematics?

A: Mathematics is separated from the empirical sciences by its a priori nature. Unlike in science, facts of mathematics are deducible through pure reason — no empirical observation is required. This makes it possible to explore mathematics in a unique way. In a famous story from Plato’s "Meno," Socrates asks a series of guiding questions to a slave who, in dialogue with Socrates, discovers a mathematical fact through pure thought. This story demonstrates the quintessential a priori nature of mathematical investigation — it is a wholly non-empirical affair. I have felt that as one dives deeply into a particular mathematical question, one begins to mentally construct and live in a kind of platonic universe — a universe of abstract objects, the exploration of which parallels the way science explores the physical world. This is what makes mathematics feel special to me; it truly feels like exploring another universe, far more abstract than the physical universe, sometimes wonderfully organized, other times infinitely chaotic, but always governed precisely by nothing more than the basic laws of logic.

Q: What is something you learned while at ASU — in the classroom or otherwise — that surprised you, that changed your perspective?

A: I think the two philosophy classes I took with Dr. Jeffrey Watson, Contemporary Analytic Philosophy and Theory of Knowledge, significantly influenced my perspective and my life. The topics investigated in Contemporary Analytic Philosophy gave me new ways of thinking about logic, language, ethics and subjective experience. The topics investigated in Theory of Knowledge led to me writing my term paper on the epistemology of mathematics, where I developed ideas that now motivate and guide my desired mathematical research direction.

Q: What are your plans after graduation?

A: I have just finished applying to graduate schools and will (fingers crossed) start graduate school in fall of 2023. My intended research direction is to investigate the use of computer systems to verify mathematical theorems from the basic axioms of logic and set theory. I am further interested in the potential use of software to not only verify proofs, but also to actively assist in discovering proofs. Mathematics has long been axiomatized by the ZFC, which means that every theorem is in principle derivable from ZFC and basic logic. But, in practice, this derivation is not done — it would be tedious and, in many respects, not useful. However, for epistemic reasons, I think it is important for modern mathematics to be verifiably derivable from some kind of axiomatic system, not just in principle, but in practice. This kind of software for verifying mathematical theorems can also be turned toward verifying the correctness of, for example, computer programs. Verifiably-correct software is of immense practical interest for many applications; two examples of catastrophic software failures are the Ariane flight V88 crash and the more recent Boeing 737 MAX disasters.

Q: Which professor taught you the most important lesson while at ASU?

A: I took my first graduate-level course with Dr. Hal Kierstead. It was a graph theory course. I was struck by his steady and methodical style of presentation. He does not attempt to make fast conclusions or skip over steps, and is very precise in what he says and what he writes. I have often made mistakes by thinking too fast or skipping over steps in arguments that I think are “obvious,” so I have been trying more to emulate Dr. Kierstead’s steady, methodical approach, both in how I do mathematics and in how I teach/explain mathematics to others.

Q: Would you recommend the mathematics program at ASU to other students?

A: I would certainly recommend the mathematics program here, mainly because of the fantastic professors. It is clear that every professor I’ve had has cared about teaching, and it definitely comes through in the quality of instruction.

Q: What is the best piece of advice you would give to those still in school?

A: While industrial society is ostensibly motivated to increase our level of luxury and comfort, it tends to also create a kind of spiritual discontentment. I think the way to combat this — and something I should have done more often — is to find time to be in nature, in a very intimate sort of way. There is more to life than the confines of industrial society.

Q: What was your favorite spot on campus, whether for studying, meeting friends or just thinking about life?

A: I am certainly very fond of Wexler Hall, having spent so much time there. It’s cozy.

Q: What do you like to do in your spare time for fun?

A: I play piano, when I can. I’d like to get back into playing tennis. I’d also like to start reading more philosophy; I have many books lined up.

Q: What do you think is most misunderstood about math by the general public?

A: That mathematics is still happening. Many people seem to think that all the important mathematics has already been done. But new mathematics is being published every day. For those who only care about practical applications, it can be noted that a lot of new mathematics is indeed practically applicable. I would also note, however, that it took many results in number theory hundreds of years before they found crucial applications in the cryptographic systems that allow the internet to function; no mathematical result should be discarded simply because it does not appear to have any current practical applications.

Q: If someone gave you $40 million to solve one problem on our planet, what would you tackle?

A: I would probably try to tackle something in education. At present, mathematics as taught by the standard K–12 curriculum misses a lot of the beautiful, creative, problem-solving aspects of mathematics. Geometry is perhaps the exception; I have had friends express their dislike for mathematics — except for geometry. I think the public’s perception of mathematics would be very different if kids were exposed to a broader selection of mathematical subjects. Elementary group theory, for instance, is something that I certainly think can be understood, at least in a basic way (say, investigating the symmetries of concrete objects), by pre-college students. The investigation doesn’t have to be deep — the point is to give kids a sense of how broad mathematics can be, rather than pigeonhole mathematics into a very particular sequence of classes.