| Contents | AI-driven systems in 2026 "solved" open problems faster than any referee can read them, many with machine-checked certificates in Lean. Mathematicians are still working on what to trust and who is responsible for checking. At this inflection point, let's throw a question: can AI read research-level mathematics the way a referee does? I will present an AI-based reviewing system for you to try out, in which distinct AI models read your paper independently. Their findings are reconciled into a single report, objections found to be mistaken are dropped, and references are checked against scholarly databases. Note that, by default, our system does not use AI providers that retain your paper. So try it on mathematics that matters to you, such as your own arXiv preprint or a draft in progress, and judge for yourself which comments help and which mislead. A referee may ask whether the assumptions are stated, the definitions consistent, and the arguments really hold tight.
On the other hand, a proof assistant caters only to the formal statement it is given; it cannot tell whether that statement is what it was supposed to mean. Recent audits find such mismatches in a large share of benchmark statements, which raise concerns on AI systems claiming to have "solved" problems whose formal versions had quietly lost the original meaning. This gap was also observed in our own effort to formalize math textbooks in-context, and taught us via these controlled experiments once more: a single AI reading is not a verdict.
I will close with some thoughts on what will matter more in the uncertain realm where the boundary between mathematics and AI will get more hazy, based on my experience in Korea University and AIML@K since 2020.
|
