Exact Mathematics with AI @ExactMathAI

@fluffydog_bow 近接分野の専門家から見てもめちゃくちゃ非自明です。平易な道具立てでここまでできるのは本当にすごい。

A picture of the switching argument at the heart of the proof.

We published a second note on OpenAI’s Banach-space papers, following our Tingley note. It reconstructs the reflexive FPP proof. Its elegant ordered-tree mechanism, carried further, gives the weak fixed point property for Banach spaces with the RNP. exactmathematics.org/topics/fixed-p…

3/3 The choice of tools can change how we understand a classical theorem. Rather than asking AI to explain a given proof, we asked it to help build one from the tools we wanted to use. For a theorem used across different fields, another route to understanding is worth sharing.

2/3 Exploring existing methods led to a proof using commuting linear operators and polynomial approximation. Stone–Weierstrass supplies the approximation; the rest is elementary. No topological degree or homology is used. We drafted and revised the entire note with ChatGPT.

1/3 Could we prove Brouwer’s fixed-point theorem with tools familiar from functional analysis? We explored this question with AI and have published a 13-page note, continuing through to Schauder’s theorem. exactmathematics.org/topics/brouwer…

3/3 既知の定理でも、どの道具で証明するかによって、理解のしやすさは変わります。 今回は、既存の証明の説明ではなく、使いたい道具から証明を組み立てることをAIに求めました。分野をまたいで使われる定理だからこそ、こうして理解の道筋を増やせることには意味があると思います。

2/3 既存の手法を探るうちに、可換な線形作用素と多項式近似を使う証明にたどり着きました。 多変数の多項式近似はStone–Weierstrassの定理から得られます。そのほかは初等的な議論で進み、写像度やホモロジーは使いません。原稿も全編ChatGPTで執筆・改訂し、読みながら説明を詰めました。

1/3 ブラウワーの不動点定理を、関数解析の道具だけで証明できないか。 位相幾何学の定理ですが、主張は関数解析的にも見える。この問いをAIと考え、シャウダーの定理までたどる解説記事を公開しました（英文13頁）。 exactmathematics.org/topics/brouwer…

AIと数学の関係を、単に「AIが何を解いたか」だけで終わらせず、人がその内容を理解し、検証し、再利用できるところまで含めて考えています。 Exact Mathematics with AIでは、AIを用いた数学研究、形式検証、そしてAIが提示した数学を人が追える形に再構成する仕事を進めています。

Official account for Exact Mathematics with AI — an independent research initiative for mathematical discovery, formal verification, and human understanding. Updates will be posted selectively. exactmathematics.org

OpenAIのバナッハ空間論に関する論文を読み解く取り組みを進めています。Tingley問題に続いて、反射的Banach空間のfixed point propertyの35頁の解説を公開しました。元論文のtree構成をさらに追うと、RNP空間のweak fixed point propertyまで得られます。 exactmathematics.org/topics/fixed-p…

An important step for the mathematics community. AI-assisted results need not only evaluation, but explanations and source records that people can inspect, understand, and reuse.

Simons Foundation @SimonsFdn

a week ago

How can the math community forge the best path forward in the AI age? We're committing $15M to workshops and initiatives — plus free AI computing resources for foundation-supported researchers — through new partnerships with @AnthropicAI and @OpenAI: bit.ly/4zpfIbW

56 131 798 813K 198

2/2 The aim is not to argue that human mathematicians are indispensable, but to explore what AI can already do. This experience suggests that we may be underestimating its capabilities—and have more to learn about bringing them out.

We've published a 21-page expository note on OpenAI's preprint on Tingley's problem. Prepared with ChatGPT, it explains the proof's structure and key geometric steps. Enjoy math with AI! exactmathematics.org/topics/tingley…

1/2 A note on how this exposition was made: ChatGPT wrote the entire manuscript and developed its structure and proof simplifications, guided by a mathematician's feedback on logical flow and readability.

MathlibAnnex v0.4.0 is public. Four Project views connect to a whole-library Catalog of 64 canonical Declaration Cards: 11 Mankiewicz, 33 Rosenberg, and 20 Naimark. exactmathematics.org/mathlibannex/

What has actually been checked? Exact Mathematics records literature search, human review, formal checking, text–formal-source correspondence, explanatory material, and public release separately. exactmathematics.org/verification/