^^AI matematica.

Precedenti

2024/25 AlphaGeometry. AI at the IMO International Mathematical Olympiad.

2026-03-04Aletheia yt 12:10 long

is a long horizon research agent bilt on top of Gemini 3 deep think.

oss: The capacity to learn from errors is so beautiful! but costly too!

https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/

2026-02-28 yt 1:11:53 - 1:15:00 3:07

2025-03-27 yt Aletheia 2 minutes paper.

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

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

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

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

dimostrare che la composizione di funzioni, e' identico a dimostrare la composizioni di implicazioni (cieo' l'implicazione e' transitiva)

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

AI matematica

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

https://aristotle.harmonic.fun/ e' Aristotle
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'.

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

wp/Fejér's_theorem

Tsumura’s 554th problem

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