2024/25 AlphaGeometry. AI at the IMO International Mathematical Olympiad.
rob: Della soluzione della congettura di Erdos fatta da AI seppi 1 mese dopo, anche se stavo aspettando un risultato matematico ritenuto di livello di un ricercatore maturo.
Una illustrazione video con valutazione e' yt , ho dovuto rallentare il video 0.75x poiche' parla troppo veloce.
Dichiarazione originale: openai/model-disproves-discrete-geometry-conjecture
Per quanto riguarda la confutazione della congettura di Erdős: sappiamo che la macchina è stata guidata verso direzioni di ricerca mai battute (i matematici che si erano dedicati alla congettura cercavano di dimostrare che fosse vera), e scoraggianti; quello che il gruppo di OpenAI ha fatto è stato far perseverare la macchina in quella direzione, finché non ha prodotto un'idea che sembrava corretta, e che comunque è stata formalizzata da esperti umani. Insomma, mi sembra molto generoso dire che il modello di OpenAI abbia risolto il problema, come se il prompt fosse stato semplicemente :"Lavora a questa congettura"; e la macchina avesse sputato fuori, dopo qualche tempo, un controesempio completo e formalmente ineccepibile. Inoltre, non credo ci sia bisogno di spiegare che OpenAI è in pesante conflitto di interessi, e che la sua narrazione dei fatti non può essere ascoltata senza un pizzico di spirito critico.
metodica spiegazione dei passato e della situazione attuale, bene e sintetica documentata, in cui si accenna al recente risultato matematico sulla Congettura di Erdos: punti equidistanti tra loro.
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!
2026-02-28 yt 1:11:53 - 1:15:00 3:07
2025-03-27 yt Aletheia 2 minutes paper.
(3:50 Spark Session, Heidelberg Laureate Forum)
new AI trained by current AI
es: GPT4 data for training GPT5
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.
open-source automated formal proof generation
large language model (LLM), state-of-the-art (SOTA) performance
A conversation with Terry Tao interessante
rob: non so se questa startup sopravvivera'.
leanprover.zulipchat.PrimeNumberTheorem/Fejér's theorem
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