>>898
>>しかし、私は定期的にロンドン数論セミナーに参加しているが、ほとんどの週に、リーンはセミナーで発表された結果を述べるのにさえ十分な現代数学の定義を知らず、ましてやそれらの証明を確認することなど到底できないと気づく。

ChatGPT 2022年11月30日
これ以前の文章と これ以降の文章は 峻別されなければならない
下記 In 2024, Google DeepMind created AlphaProof[28]は、数オリ the level of a silver medalist
実際 AIで東大入試を解かせた記事がある
2025年は さらにレベルアップだろう

https://news.yahoo.co.jp/articles/9e1ac52a521e764a445abcd904c82d32309946b5
AIが東大理科3類「合格水準」　25年入試、最低点を上回る 4/5 共同通信

https://ja.wikipedia.org/wiki/ChatGPT
ChatGPT
概要
2022年11月30日、ChatGPTはプロトタイプとして公開され、

https://en.wikipedia.org/wiki/Lean_(proof_assistant)
Lean (proof assistant)
History
In 2025, ACM SIGPLAN Programming Languages Software Award was awarded to Gabriel Ebner, Soonho Kong, Leo de Moura and Sebastian Ullrich for Lean, cited for its "significant impact on mathematics, hardware and software verification, and AI".[7]
Usage
Mathematics
See also: Proof assistant § Notable formalized proofs
Lean has received attention from mathematicians such as Thomas Hales,[15] Kevin Buzzard,[16] Terence Tao,[17] and Heather Macbeth.[18] Hales is using it for his project, Formal Abstracts.[19] Buzzard uses it for the Xena project.[20] One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of Imperial College London in Lean. Tao released a Lean companion to his Real analysis textbook Analysis I, consisting of a formalization of selected sections of the mathematical text.[21] Macbeth is using Lean to teach students the fundamentals of mathematical proof with instant feedback.[22]

Artificial intelligence
In 2022, OpenAI and Meta AI independently created AI models to generate proofs of various high-school-level olympiad problems in Lean.[25] Meta AI's model is available for public use with the Lean environment.[26]

In 2024, Google DeepMind created AlphaProof[28] which proves mathematical statements in Lean at the level of a silver medalist at the International Mathematical Olympiad. This was the first AI system that achieved a medal-worthy performance on a math olympiad's problems.[29]

In April 2025, DeepSeek introduced DeepSeek-Prover-V2, an AI model designed for theorem proving in Lean 4, built on top of DeepSeek-V3.[30]