2024/25 AlphaGeometry. AI at the IMO International Mathematical Olympiad.
Per mentalizzare, capire il senso della congettura, ricordiamo:
occorre considerare tutte le derivate parziali possibili, che sono
organizzate in una matrice, detta jacobiana
Teo: se il determinante jacobiano e' continuo e diverso da zero in un intorno,
allora e' invertibile nell'intorno.
Levent Alpöge at Harvard University wrote on X
hello there the jacobian conjecture is false thanx to my close friend akhil for asking about it and my other close friend fable for working during the world cup final
((1+xy)^3 z + y^2 (1+xy) (4+3xy), y + 3 x (1+xy)^2 z + 3 x y^2 (4+3xy), 2 x - 3 x^2 y - x^3 z): \C^3\to \C^3, has jacobian determinant -2, and sends (0, 0, -1/4), (1, -3/2, 13/2), and (-1, 3/2, 13/2) to (-1/4, 0, 0)
cmt:
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.
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