In modern society, finance, telecommunications, and logistics systems all operate on large-scale computer networks. Computational power has now become the core infrastructure of civilization. 

People were shocked when humans were surpassed in Go. This is because machines have surpassed human top players in a game of calculation and intuition. However, Go is a game where victory or defeat is evident.

Mathematics is different. Mathematics is not a discipline of arriving at answers, but a discipline of proving why something is true.

The World of Proof Enters the Machine Realm

Artificial intelligence is now moving beyond calculation into the realm of proof.

Google DeepMind, Google's AI research organization, announced in 2024 that AlphaProof and AlphaGeometry 2 solved four out of six problems in the International Mathematical Olympiad (IMO), achieving a silver medal level.

A subsequent paper published in Nature also explained that the system scored 28 out of a possible 42 points, achieving a silver medal performance.

In 2025, they took a step further.

Google DeepMind announced that Gemini Deep Think solved five out of six problems in the International Mathematical Olympiad, scoring 35 points and reaching a gold medal level.

Reuters also reported in July 2025 that AI models from Google and OpenAI achieved gold medal level performance in the International Mathematical Olympiad. However, it is important to distinguish that OpenAI's results were from a separate evaluation, not an official participation.

The score is not the only important aspect. AI achieving success in mathematics does not simply mean it got the answers to difficult problems correct. It signifies that machines have entered the domain of proof, considered the most rigorous area of human reasoning.

Mathematics has long been considered the last bastion of human intellect. Logic was more important than the correct answer, and verification was more important than logic. Now, AI is beginning to enter the verification process as well.

Who Verifies the Machines?

Mathematical proof is a form of trust contract. When a mathematician announces a new theorem, other mathematicians read the proof, find errors, and examine logical gaps.

If no counterexamples emerge over time and the community accepts it, the proposition becomes part of mathematical knowledge. The authority of mathematics does not stem from individual fame but from verifiable logic and community acceptance.

This is why AI is shaking up this structure.

There are proofs generated by AI. Even formal verification programs have deemed them error-free. But what if human mathematicians cannot intuitively grasp the overall flow of the proof?

If humans accept a proof deemed correct by a machine, is it knowledge understood by humans, or knowledge guaranteed by a machine?

The term "formal verification" is crucial here.

Formal verification involves translating mathematical propositions and proofs into a rigorous language that computers can read and checking if the proof is correct according to logical rules. Systems like Lean (a mathematical proof assistant) are prime examples.

The official introduction of Lean describes it as an open-source programming language and proof assistant that enables "correct, maintainable, and formally verified code."

On the surface, this seems beneficial for mathematicians.

Machines can identify logical gaps that humans might miss. They can also quickly examine vast numbers of cases and suggest new patterns or conjectures. If the lengthy verification process is accelerated, the pace of mathematical research can also increase.

However, speed does not equate to understanding. Mathematics is not merely a mechanical procedure for distinguishing between true and false. It is a process of understanding why a certain structure holds, how that proposition relates to other theories, and how it can be generalized.

The discovery of a proof by AI does not automatically lead to human comprehension.

At this point, an old question in mathematics is revived.

What constitutes a proof? Is being logically flawless sufficient? Or must it be an explanation that humans can comprehend? Do long proofs verified by computers hold the same authority as short proofs understood by humans? If a proof created by a machine is true, who interprets the meaning of that truth?

Questions Remaining for Humans

AI pushes this question beyond mathematics.

Today's society is already moving in a direction that relies on verification processes rather than understanding.

Financial transactions operate on cryptography and algorithms. Medical diagnoses and drug development also rely on data and model judgments. Election systems also depend on computational procedures and verification mechanisms.

A structure is expanding where people accept outcomes if the procedures are trustworthy, even if they cannot personally understand every step.

Mathematics is the most rigorous testbed for that trend.

If, even in mathematics, humans begin to rely on machine verification without directly understanding all proofs, larger changes are inevitable in other fields of knowledge.

Scientific papers, legal judgments, financial risk analyses, and policy simulations all face the same question. To what extent can humans accept conclusions presented by AI?

However, there is no need to view AI solely as an intruder in mathematics. Rather, AI is closer to a new verification tool than a competitor to human mathematicians.

Just as calculators replaced mental arithmetic without eliminating mathematics, proof-assistance AI is more likely to change the role of mathematicians than eliminate them.

Humans no longer need to repeat all calculations and verifications manually. Instead, they must decide what questions to ask, which proofs are meaningful, and which results to adopt as knowledge.

This change also impacts education.

In the future, mathematics education may no longer be sufficient with just training to quickly find answers. In an era where AI provides solutions, "Why can we trust this answer?" becomes more important than "Did you get the answer?".

Students will need to become verifiers rather than calculators. The ability to find logical gaps may become more crucial than the ability to memorize solutions.

From an ALO (AI Linked Optimization) perspective, the core of this change is clear.

AI can assist in the production and review of proofs. However, the decision of which proofs to adopt as knowledge, which explanations to teach, and what potential for error to accept remains within the human domain.

While mathematics has entered the AI era, the ultimate responsibility for accepting truth cannot be handed over to machines.

AI is shaking up mathematics not because of its computational power, but because it forces us to re-examine the structure of verification: what humans recognize as true.

Mathematics may appear to be a discipline of answers, but it is, in fact, a discipline of trust. And trust cannot be manufactured by machines. Machines can assist in verification, but the final decision to transform verification into trust rests with the human community.

Mathematics in the age of AI is not a defeat for human reason. Rather, it more clearly shows where human reason should remain. Calculations can be done by machines. Proofs can be assisted by machines.

However, the responsibility for formulating questions, interpreting meaning, and accepting truth remains with humans.

Mathematics has entered the AI era. The important question now is not whether AI can produce proofs, but who will verify those proofs, who will accept them, and who will be responsible.

❄ This article was published in the 9th issue (2nd week of May) of The Weekly Hankook-Ilbo.