AutoRes_Math

AutoResはAIによる自動研究を目指す有志団体です。
このアカウントではAI4Mathに関連する情報をまとめます。
Zenn:

[AutoRes_Math @AutoRes_Math]

【ブログ更新】今年の東大理系数学をAIがLeanで形式証明できるか検証しました。Harmonicの自動定理証明システムAristotleにTeX入力で解かせたところ、6問中4問を完答・残り2問も部分正解という結果でした。
https://t.co/PIR5xOamES

[Bartosz Naskręcki @nasqret]

AI technology is on the rise. So are its applications in industry, science, and society at large. At

https://t.co/MwavD3OUwM

we, a group of 16 scientists, including mathematicians, computer scientists, philosophers, and historians, have drafted a declaration calling for action on the challenges posed by the use of artificial intelligence in mathematical research.

Over several months, we carefully weighed the promises and risks of introducing AI into research workflows and beyond. The declaration has already been endorsed by international communities, most prominently by the International Mathematical Union, as well as by a large group of mathematicians and other scientists.

We invite our colleagues to sign the declaration and support its recommendations on how AI should be adopted in our workflows, and how we should establish and maintain relationships with AI labs and industry.
One of its central points is the need to preserve balance, rigor, and sound judgment while acknowledging the extraordinary pace of development in the AI community.

We hope this declaration, a deeply human act, will serve as a guiding document for those who recognize the human imperative and the need for governance in scientific discovery, especially mathematical discovery.

[ほら/hora @hora_algebra]

事例交換/技術的質問をする会を6/4 or 6/5で(東京 + online?多分...)でやる話になっているので，ご興味ある方���ぜひ．

[OpenAI @OpenAI]

AI can give researchers the freedom to pursue “crazier” ideas.

For Terence Tao, AI creates more room to experiment, test unexpected paths, and discover what might otherwise stay out of reach.

[OpenAI @OpenAI]

Today, we share a breakthrough on the planar unit distance problem, a famous open question first posed by Paul Erdős in 1946.

For nearly 80 years, mathematicians believed the best possible solutions looked roughly like square grids.

An OpenAI model has now disproved that belief, discovering an entirely new family of constructions that performs better.

This marks the first time AI has autonomously solved a prominent open problem central to a field of mathematics.

[Timothy Gowers @wtgowers @wtgowers]

If you are a mathematician, then you may want to make sure you are sitting down before reading further.

[Acer @AcerFur]

FYI, if you are submitting an AI-generated/assisted solution to an Erdős problem, please take the time to understand the argument enough that you should be able to distil the general ideas and be able to be happily questioned on said points. Also, ideally, write the PDF yourself.

[富谷(AI×物理)/東女(准教授)/京大/理研 @TomiyaAkio]

生成AIで科学がどう変わるのか、気になりますよね…?

6/12（金）に研究会「生成科学：生成AI時代の科学の姿を探る」を開催します。物理・生命・数学など、分野をまたいで喧々諤々と議論します。

��地・Zoomのハイブリッドです。
https://t.co/dNMcY2wYO2
面白いと思いますのでぜひに。

[Amaury Hayat @Amaury_Hayat]

For the last few months, we’ve been building a proving agent with the Numina Project. Recently, it found a proof of a conjecture in control theory that I had attempted to prove while a PhD student, and that I had not managed to solve. It had remained open since then (1/15)

[Jaynit @jaynitx]

Terence Tao: "Previously, you needed a PhD to contribute to math research. Now a high school student can."

Dwarkesh asks the world's most famous mathematician: what's your advice for someone considering a career in math, especially in light of AI progress?

Tao is honest about uncertainty:

"We live in a time of change. A particularly unpredictable era. Things that we've taken for granted for centuries may not hold anymore. The way we do everything... not just mathematics... will change."

He admits his preference:

"In many ways, I would prefer a much more boring, quiet era where things are much the same as they were 10 or 20 years ago. But one just has to embrace this. There's going to be a lot of change. The things you study... some of them may become obsolete or revolutionized. But some things will be retained."

On new opportunities:

"Previously, you had to go through years and years of education and get a math PhD before you could contribute to the frontier of math research. But now it's quite possible at the high school level that you could get involved in a math project and actually make a real contribution... because of all these AI tools and Lean and everything else."

His advice:

"There will be a lot of non-traditional opportunities to learn. You need a very adaptable mindset. There'll be worth pursuing things just for curiosity and for playing around.

Still go through traditional education and learn math and science the old-fashioned way for a while... credentials will still be important. But you should also be open to very, very different ways of doing science. Some of which don't exist yet."

He concludes:

"It's a scary time. But also very exciting."

[Yahoo!ニュース @YahooNewsTopics]

【数学の未解決問題 AIが相次ぎ解く】
https://t.co/B4zfdNUbJM

[Bartosz Naskręcki @nasqret]

I think a radical new viewpoint is emerging on the many activities that mathematicians do. Perhaps a novel profession of mathematical engineering is emerging from the early chaos of AI for mathematics.

I can see very clearly that the coordination, setup, technical pursuit, and orchestration of AI systems scaled for massive mathematical efforts and projects will require a special engineering mindset that is currently lacking, or almost completely absent, in mathematical projects.

The existence of such a profession is not in opposition to mathematical tinkerers who use their artisanal craft to produce genuinely novel content. As with any kind of content, someone needs to adapt it to the grand scheme of things. This is why these roles are starting to appear complementary rather than competitive.

Maybe this is a temporary activity, soon to be replaced by computers, but I think the major role of mathematical engineers will be to stay in touch with the tinkerers and provide a human cushion around their internal activities.

I am enjoying this kind of activity (*), where you orchestrate with models and see how the project itself becomes a challenge in design and scale. This might well mean more jobs for mathematicians.

In the long run, I suspect we may become secondary cognitive powers in parts of the mathematical information chain. But I do not think this will happen very soon across the whole system. And I hope it never happens at the most human layer: the joy people feel when a new idea is born.

(*) This project is essentially a lambda-calculus lab, fully integrated with classical topics such as Church’s lambda calculus, the Aristotle formal proofs system, and extensions over particular papers. I presented it to students at the workshop in Warszawa-Falenty and was very pleased with the result. I am now using this framework for proof development. What strikes me most is that this is primarily an engineering challenge: the mathematics entering the pipeline is being handled, structured, and formalized, but not radically developed inside the pipeline itself.

[折池雄太 @YutaOriike]

エルデシュ問題#514の第3問について自然言語証明と形式化を行いました。フォーラムのステータスが partial から solution になっているため、じきに OPEN から PROVED に変わるのではないかと思います。githubの方でも名前が載りました。
https://t.co/4wBi8CViVO

[Nyx Foundation @NyxFoundation]

【論文発表のお知らせ】

「Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization」がAIPV2026に採択されました。

https://t.co/tjxlUQzcVd

AIが生成する形式数学証明、その「意味」は誰が保証するのか？

私たちは、AIが証明を、人間が意味を、定理証明器が論理を担うという役割分担を提案します。

定理証明支援系の型検査が保証するのは、命題に対して証明項が論理的に正しく構成されていることのみです。

命題のステートメントや定義が意図された数��的内容を表しているかは検証されません。

本稿ではこのギャップを意味的ハルシネーション(semantic hallucination)と定義しました。

AIが「3/2 = 1.5」をLeanに書き起こす際、型注釈を落とすと自然数として解釈され、「3/2 = 1」という命題が型検査を通過し証明まで完結してしまう、こうした「論理的には正しいが意味的には誤った」形式化が、AI生成証明には潜みうるのです。

これに対して私たちは、Lean4プロジェクトの依存グラフを型依存と値依存に分けて可視化する対話型WebビューアLean Atlasを開発しました。

中核となるアルゴリズムLean Compass は、証明の論理的正しさにだけ関わる依存を安全に取り除き、定理の意味に影響しうる部分だけを残します。

これにより、人間が意味的にレビューすべき範囲を大幅に絞り込めます。数千ノード規模のプロジェクトでも、人間がレビューすべき範囲が劇的に絞り込まれます。

構造の異なる6つのLean4プロジェクト(PrimeNumberTheoremAnd、Carleson、Brownian Motion、FLT、PhysLib、XMSS Encoding Scheme)で評価しました。

証明中心のプロジェクトでは平均94–99%のノード削減を��成��ました。

最大規模の Carleson では2,000ノード近い依存グラフが5ノードまで縮小される例も観測されています。

さらに理論物理学(PhysLib 69.0%)と耐量子暗号(XMSS 27.3%)にも適用可能であることを示し、本フレームワークが純粋数学を超えた科学分野の形式検証にも展開できることを実証しました。

私たちは、人間による意味的検証を経た形式化コードを意味整合的Leanコード (aligned Lean code) と定義し、AI生成形式化の新たな品質基準として提案しています。

型検査の通過率では捉えられない「意味的な正しさ」を、AIと人間が分担して保証し、その人間側の負担を実用的な規模まで圧縮する基盤がLean Atlasです。

意味整合的Leanコードを蓄積することで、AI の学習データおよび数学者の参照資源として機能する形式化コードベースを築く、これが私たちが目��す human-AI 協調形式化の未来像です。

[Stat.ML Papers @StatMLPapers]

Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models https://t.co/MFX6HO0UQW

[Przemek Chojecki | PC @prz_chojecki]

GPT-5.5 Pro is really on the next level.

In the past 3 days there are like 8-10 claimed solutions to new open Erdos problems with GPT-5.5.

That doesn't mean all are valid and will be accepted, but the last time we had a similar activity was in December/January with GPT-5.2 (and even then there was less claims and not as fast).

Also these claims right now are for harder problems, because all Erdos problems were scanned with GPT-5.2 at least briefly. This means that GPT-5.5 is a level above 5.2, and probably half a level above 5.4.

Solutions that surface are more involved/interesting.
I've browsed a couple and they all seem plausible.

5.5 got considerably better at synthesis of various arguments from various sources and doing it in a more effective way.

I'm pretty sure we're going to see even more spectacular applications soon.

However we're still pretty far away from AI being at a proper research-level.

My move 37 in mathematics would actually be a new definition, not a proof. I need to see an LLM define a new concept that would simplify or connect various existing structures and give raise to a new theory. But perhaps this would be synonymous with AGI.

[Lean @leanprover]

Great to see Lean at the centre of this closed loop: from autonomous discovery, to formal verification, to mathematical exposition that humans can read, rewrite, and improve.

[AutoRes_Math @AutoRes_Math]

https://t.co/v5nFziuNGg

[AutoRes_Math @AutoRes_Math]

2026/4/28 テレンス・タオ氏の投稿まとめ

数学は「証明の希少性の時代」から「証明の豊富さの時代」へと移行しているが、数学のインフラと文化はまだそれに適応していない。

1. 三つの構成要素のインピーダンス・ミスマッチ

数学的問題解決には3つの段階があり、AIによって最初の段階だけが急加速したため、不均衡が生じている。

・証明の生成(proof generation): AIにより爆発的に増加
・証明の検証(proof verification): 追いついていない
・証明の消化���理解(proof digestion): 追いついていない

具体例として、エルデシュ問題サイトでは、GPT-5.5のリリースとエルデシュ問題#1196の解決以降、評価待ちの主張された解答が約20件も滞留している(以前は常時1〜2件程度だった)。

2. 料理のアナロジーによる説明

タオ氏はこの状況を「食料」に例えて説明している。

< 数学と料理の対応関係>
- 証明の生成 → 食料の収集 　
- 証明の検証 → 食料の洗浄・検査 　
- 証明の消化 → 調理

食料が希少な社会では、食料を持ち込む狩人・農民が最も称賛される。どんな素材でも歓迎され、誰かが調理を引き受ける。

食料が豊富な社会では、見知らぬ人が処理されていない肉の塊を持ち込んでも歓迎されない。よく調理され、信頼できる人が作った料理が重視され、その周りでの会話や次世代の育成が大切にされる。

3. 逆説的な現状

証明生成が大幅に加速したにもかかわらず、数学の進歩自体は加速していない。なぜなら、AIに指示を出した人が「検証や要約をする時間がない」ままの「生の」証明が大量に投下されているから。

こうした貢献は問題への議論を実質的に進めないだけでなく、「もう解かれた」と見なされて問題への関心を逆に殺してしまうという負の影響すらある——たとえ誰一人としてその解を理解していなくても。

4. タオ氏の予測と提言

- 証明を最初に生成したことに対する名声の一部は、検証・消化を担う人々へ移転される必要がある。
理想的には、生成・検証・消化を同じ著者グループが担うべき。
- 現代社会が生の食材を「食事」と見なさないのと同様に、数学界も「生の」「未消化の」証明を「問題の解答」とは���なさなくなるだろう。
- 重要なのは個別の問題の解決��のものではなく、分野全体がその貢献によってどう豊かになるかである。

[Sebastien Bubeck @SebastienBubeck]

Ramsey numbers are one the most basic objects in combinatorics, a beautiful illustration of structure within chaos. They have been heavily studied for almost a century now, so it came as a real surprise to us when an internal version of GPT-5.5 proved a new elementary result about them:

\lim_{n\to \infty} R(k,n+1)/R(k,n) = 1 for all k

This was also known as Erdos problem #1014, although I personally think the more relevant bit is that it's a basic result about off-diagonal Ramsey numbers.

As it often happens (for now), the proof is reasonably simple in hindsight, although it is quite a wire act and it relies on some unexpected numerics (the "unexpected" part here is probably why this wasn't discovered before). Despite being simple, it's certainly the type of result that could now be taught in a combinatorics class.

Pdf of the proof (produced by @mehtaab_sawhney):
https://t.co/xhkopmWmW4

Lean verification of the proof (produced by Boris Alexeev):
https://t.co/Uqm0tZjnTm

[Alex Meiburg @Timeroot]

The Lean language (@leanprover) has utilities for verifying software, and AI is adept at using it. But can AI prove correctness for a *foreign architecture* with *no existing API*? It turns out, yes!

@HarmonicMath's Aristotle wrote a z80 emulator:
https://t.co/ZFWUXaAIIf (1/n)