^^AI matematica.

 

2025-09-15 Superhuman AI Mathematicians - Sanjeev Arora

(3:50 Spark Session, Heidelberg Laureate Forum)

new AI trained by current AI

es: GPT4 data for training GPT5

The dream of automating math

AI self-improvement (and why math is well suited for it).

  1. Checking proof is efficiente (is in P polinomial time): se riesci a fare una dimostrazione, e' facile verificarla, esiste LEAN, proof assistant.
  2. The AI itself can generate very good question.

 

2025-04-05 Goedel-Prover https://goedel-lm.github.io/

open-source automated formal proof generation

large language model (LLM), state-of-the-art (SOTA) performance

2025-10-01 arxiv Aristotle: IMO-level Automated Theorem Proving

  1. https://aristotle.harmonic.fun/   e' Aristotle
  2. yt Aristotle: IMO-level Automated Theorem Proving. AI generated.

Gauss, agent for autoformalization www.math.inc

A conversation with Terry Tao  interessante

rob: non so se questa startup sopravvivera'.

 

yt t=391 Emily Riehl — The future of mathematics | Math, Inc.

I mean formalization has completely changed my view of what mathematics is. ...

principalmente dovuta a usare come fondamenti della matematica la teoria dei tipi dipendenti piuttosto che la teoria degli insiemi.

Approfondire sulle chat

2026-01-07 application of AI to Erdos problems

mathstodon/@tao

2024-5-6 PNT PrimeNumberTheorem, and beyond

leanprover.zulipchat.PrimeNumberTheorem/Fejér's theorem

  1. wp/Fejér's_theorem

Tsumura’s 554th problem

  1. 2025-10-06 nednex/two-notorious-math-problems-fall-to-llm-tsumuras-554th-solved-majority-optimality-disproved/
  2. 2025-10-05 facebook/gpt-5-pro-just-solved-the-math-problem-that-no-other-llm-could-solve-took-14-min

Answer to Yu Tsumura’s 554th problem:

Given xy² = y³x and yx² = x³y, derive x y^{2n} x⁻¹ = y^{3n}.

x y² x⁻¹ = y³  moltiplicando  membro a membro 

                   xy²x⁻¹ xy²x⁻¹  = y³ y³  sviluppando

x y⁴ x⁻¹ = y⁶   ripetendo il procedimanto

x y⁶ x⁻¹ = y⁹            yx⁶y⁻¹  = x⁹

 

For n=3: y⁹ = e.

Matching orders of y² ~ y³ ⇒ y = e.

Then x³ = x² ⇒ x = e.

Group is trivial.

 

The paper - https://arxiv.org/pdf/2508.03685
You can check from The reasoning traces summary : - https://chatgpt.com/.../68bc7446-ca74-8007-9646-955c4e7e6daa