Numina

24 juin : en modifiant l'énoncé, échec systématique Formalization failed : final check failed : execution failed due to hitting the max turns limit. lien 23 juin, je réessaie Numina, sans espoir, le système s'arrête après 83 fenêtres de logique, sur un Final check failed : execution failed due to hitting the max turns limit (on se rappelle que Russell et Whitehead ont utilisé 360 pages pour démontrer que 1+1=2), j'abandonne cette possibilité. Un peu plus tard, je réessaie, il va au bout, mais bien sûr ne fournit pas de preuve, normal, je fais écrire à Claude un script pour générer du Latex depuis une page numina lien

23 juin 2026 : Fatalement ! je m'étais plantée dans l'énoncé en logique du premier ordre, c'eût été trop beau, snif ! lien

22 juin 2026 : Numina me dit qu'elle vient de démontrer la conjecture de Goldbach en Lean à partir d'une formalisation en logique du premier ordre (que j'avais postée sur mon site le 15 mai 2022) que je lui ai fournie lien (la formalisation de 2022 lien, la démonstration par Leila Schneps (le 4 décembre 2019) que la caractérisation que je proposais était valide lien     lien)