Thomas (lipsum.dev)
@lipsum.dev
Maths et applications, avec les mains et avec du code 💻
https://lipsum.dev
https://lipsum.dev
Je vois que CSLib a dans sa roadmap des preuves de complexité, cf www.cslib.io/roadmap/, ça sera intéressant de voir comment ils font ça.
CSLib
A Focused Effort on Formalizing Computer Science in Lean
www.cslib.io
December 1, 2025 at 8:49 PM
Je vois que CSLib a dans sa roadmap des preuves de complexité, cf www.cslib.io/roadmap/, ça sera intéressant de voir comment ils font ça.
Si j'en crois ce qui se raconte par là proofassistants.stackexchange.com/q/1976/2780, ça va être compliqué à cause de l'extensionnalité des fonctions dans Lean.
can proof assistants reason about complexity of programs?
Sorry if this question is too basic or vague, I'm new to using proof assistants.
Using a proof assistant, one can construct the type Ordered n t of ordered lists of length n over a type t, provided...
proofassistants.stackexchange.com
December 1, 2025 at 8:49 PM
Si j'en crois ce qui se raconte par là proofassistants.stackexchange.com/q/1976/2780, ça va être compliqué à cause de l'extensionnalité des fonctions dans Lean.
Avez-vous utilisé des outils particuliers d'ailleurs ? (extension de l'éditeur de texte, assistants IA, etc.)
December 1, 2025 at 7:14 PM
Avez-vous utilisé des outils particuliers d'ailleurs ? (extension de l'éditeur de texte, assistants IA, etc.)
Sinon, félicitations, vu qu'il m'a fallu plusieurs heures pour pondre un simple quicksort (gist.github.com/tchaumeny/80...) ce week-end, j'imagine que ça a pas dû être simple.
Quicksort implemented and certified in Lean
Quicksort implemented and certified in Lean. GitHub Gist: instantly share code, notes, and snippets.
gist.github.com
December 1, 2025 at 7:14 PM
Sinon, félicitations, vu qu'il m'a fallu plusieurs heures pour pondre un simple quicksort (gist.github.com/tchaumeny/80...) ce week-end, j'imagine que ça a pas dû être simple.
C'est que chez moi que Firefox ne détecte pas que c'est de l'UTF-8 ?
December 1, 2025 at 7:14 PM
C'est que chez moi que Firefox ne détecte pas que c'est de l'UTF-8 ?
« Rocquefort » pour rester cocorico 🇫🇷
November 28, 2025 at 8:12 PM
« Rocquefort » pour rester cocorico 🇫🇷
Source : youtu.be/M-MgQC6z3VU?... (à 4min26)
What was Euclid really doing? | Guest video by Ben Syversen
YouTube video by 3Blue1Brown
youtu.be
November 28, 2025 at 6:59 PM
Source : youtu.be/M-MgQC6z3VU?... (à 4min26)
Y'a quelques mois :
- Coiffeuse : Vous bossez dans quoi ?
- Moi : Dans l'informatique
- Coiffeuse : Ah, c'est dingue ce qu'on fait avec l'IA aujourd'hui. Ma belle-fille a perdu un proche récemment et elle avait un superbe discours funèbre grâce à l'IA !
- Moi : Ah.
- Coiffeuse : Vous bossez dans quoi ?
- Moi : Dans l'informatique
- Coiffeuse : Ah, c'est dingue ce qu'on fait avec l'IA aujourd'hui. Ma belle-fille a perdu un proche récemment et elle avait un superbe discours funèbre grâce à l'IA !
- Moi : Ah.
November 19, 2025 at 8:37 PM
Y'a quelques mois :
- Coiffeuse : Vous bossez dans quoi ?
- Moi : Dans l'informatique
- Coiffeuse : Ah, c'est dingue ce qu'on fait avec l'IA aujourd'hui. Ma belle-fille a perdu un proche récemment et elle avait un superbe discours funèbre grâce à l'IA !
- Moi : Ah.
- Coiffeuse : Vous bossez dans quoi ?
- Moi : Dans l'informatique
- Coiffeuse : Ah, c'est dingue ce qu'on fait avec l'IA aujourd'hui. Ma belle-fille a perdu un proche récemment et elle avait un superbe discours funèbre grâce à l'IA !
- Moi : Ah.
donc à titre personnel, j'attends toujours de pouvoir les manipuler et leur poser des questions dans différents domaines pour me faire une idée. Ceux qui sont accessibles au grand public continuent à faire des erreurs sur des choses assez simples, pour peu qu'on sorte des sentiers battus.
November 19, 2025 at 7:12 PM
donc à titre personnel, j'attends toujours de pouvoir les manipuler et leur poser des questions dans différents domaines pour me faire une idée. Ceux qui sont accessibles au grand public continuent à faire des erreurs sur des choses assez simples, pour peu qu'on sorte des sentiers battus.
OK. Il me semble quand-même que le passage en question aurait pu préciser qu'il s'agissait de modèles qui ne sont pas ceux disponibles pour le grand public (si?).
Par ailleurs, par le passé il y a eu des histoires de données d'entraînement contaminés etc. qui érodent un peu ma confiance,
Par ailleurs, par le passé il y a eu des histoires de données d'entraînement contaminés etc. qui érodent un peu ma confiance,
November 19, 2025 at 7:12 PM
OK. Il me semble quand-même que le passage en question aurait pu préciser qu'il s'agissait de modèles qui ne sont pas ceux disponibles pour le grand public (si?).
Par ailleurs, par le passé il y a eu des histoires de données d'entraînement contaminés etc. qui érodent un peu ma confiance,
Par ailleurs, par le passé il y a eu des histoires de données d'entraînement contaminés etc. qui érodent un peu ma confiance,
...différentes boîtes autour de la "suprématie quantique" a érodé ma confiance.
November 19, 2025 at 5:36 PM
...différentes boîtes autour de la "suprématie quantique" a érodé ma confiance.
J'attends de pouvoir tester ça alors, pour l'instant tous les modèles que j'ai pu tester font rapidement des erreurs quand on part dans des trucs un peu subtiles ou suffisamment de niche pour être peu présents dans la littérature.
Par ailleurs, je dois dire que par le passé la communication de...
Par ailleurs, je dois dire que par le passé la communication de...
November 19, 2025 at 5:36 PM
J'attends de pouvoir tester ça alors, pour l'instant tous les modèles que j'ai pu tester font rapidement des erreurs quand on part dans des trucs un peu subtiles ou suffisamment de niche pour être peu présents dans la littérature.
Par ailleurs, je dois dire que par le passé la communication de...
Par ailleurs, je dois dire que par le passé la communication de...
OK. Le modèle semblant ne pas être accessible au grand public et (à ma connaissance), les modèles disponibles étant loins de ces capacités, j'imagine que cela réduit le problème à une question de confiance vis-à-vis de cette communication.
November 19, 2025 at 5:29 PM
OK. Le modèle semblant ne pas être accessible au grand public et (à ma connaissance), les modèles disponibles étant loins de ces capacités, j'imagine que cela réduit le problème à une question de confiance vis-à-vis de cette communication.
...je ne sais pas si elle rentre dans les détails et si les résultats sont vérifiables, auriez-vous un lien ?
November 19, 2025 at 5:18 PM
...je ne sais pas si elle rentre dans les détails et si les résultats sont vérifiables, auriez-vous un lien ?
Je me base sur le papier www.nature.com/articles/s41... qui a été publié il y a une semaine, et qui concerne effectivement les IMO 2024.
La capture d'écran ci-dessus semble provenir d'une communication plus "corporate", ...
La capture d'écran ci-dessus semble provenir d'une communication plus "corporate", ...
Olympiad-level formal mathematical reasoning with reinforcement learning - Nature
Nature - Olympiad-level formal mathematical reasoning with reinforcement learning
www.nature.com
November 19, 2025 at 5:18 PM
Je me base sur le papier www.nature.com/articles/s41... qui a été publié il y a une semaine, et qui concerne effectivement les IMO 2024.
La capture d'écran ci-dessus semble provenir d'une communication plus "corporate", ...
La capture d'écran ci-dessus semble provenir d'une communication plus "corporate", ...
Je me permets de te taguer @thomascabaret84.bsky.social comme tu es dans la vidéo, même si ce n'est pas ta partie, il me semble important d'être précis dans la vulgarisation et ce point me semble problématique.
November 19, 2025 at 4:51 PM
Je me permets de te taguer @thomascabaret84.bsky.social comme tu es dans la vidéo, même si ce n'est pas ta partie, il me semble important d'être précis dans la vulgarisation et ce point me semble problématique.
... nouvelle version depuis, mais les grands principes restent les mêmes.
Bref, mon point central est qu'en l'état, les IA de Google qui résolvent des problèmes mathématiques difficiles et absents de leur corpus d'entraînement reposent de façon importante sur des systèmes symboliques.
Bref, mon point central est qu'en l'état, les IA de Google qui résolvent des problèmes mathématiques difficiles et absents de leur corpus d'entraînement reposent de façon importante sur des systèmes symboliques.
November 19, 2025 at 3:42 PM
... nouvelle version depuis, mais les grands principes restent les mêmes.
Bref, mon point central est qu'en l'état, les IA de Google qui résolvent des problèmes mathématiques difficiles et absents de leur corpus d'entraînement reposent de façon importante sur des systèmes symboliques.
Bref, mon point central est qu'en l'état, les IA de Google qui résolvent des problèmes mathématiques difficiles et absents de leur corpus d'entraînement reposent de façon importante sur des systèmes symboliques.
AlphaGeometry, lui, utilise un assistant de preuve spécialisé en géométrie, plus proche de la façon dont ces problèmes sont exprimés (Lean est très généraliste et la géométrie n'y est pas encore très bien formalisée).
J'en avais parlé sur mon blog ici lipsum.dev/2024-07-1-me..., il y a eu une...
J'en avais parlé sur mon blog ici lipsum.dev/2024-07-1-me..., il y a eu une...
Quelques aspects de la mécanisation de la géométrie
En début d'année 2024, des chercheurs de DeepMind annoncent AlphaGeometry :
un logiciel capable de résoudre des problèmes de géométrie posés aux Olympiades…
lipsum.dev
November 19, 2025 at 3:42 PM
AlphaGeometry, lui, utilise un assistant de preuve spécialisé en géométrie, plus proche de la façon dont ces problèmes sont exprimés (Lean est très généraliste et la géométrie n'y est pas encore très bien formalisée).
J'en avais parlé sur mon blog ici lipsum.dev/2024-07-1-me..., il y a eu une...
J'en avais parlé sur mon blog ici lipsum.dev/2024-07-1-me..., il y a eu une...
Concernant Lean (composant central de AlphaProof), il s'agit d'un assistant de preuve, c'est-à-dire en gros d'un langage de programmation pour exprimer des énoncés mathématiques, leurs preuves, et vérifier que la preuve prouve bien l'énoncé.
En voici un exemple accessible bsky.app/profile/lips...
En voici un exemple accessible bsky.app/profile/lips...
Avec l'assistant de preuve Lean :
theorem married_looks_unmarried
(H1 : Looks Paul Linda)
(H2 : Looks Linda John)
(H3 : Married Paul)
(H4 : ¬Married John) :
∃ x y : Person, Married x ∧ ¬Married y ∧ Looks x y :=
by
by_cases h : Married Linda
· exists Linda, John
· exists Paul, Linda
theorem married_looks_unmarried
(H1 : Looks Paul Linda)
(H2 : Looks Linda John)
(H3 : Married Paul)
(H4 : ¬Married John) :
∃ x y : Person, Married x ∧ ¬Married y ∧ Looks x y :=
by
by_cases h : Married Linda
· exists Linda, John
· exists Paul, Linda
November 19, 2025 at 3:42 PM
Concernant Lean (composant central de AlphaProof), il s'agit d'un assistant de preuve, c'est-à-dire en gros d'un langage de programmation pour exprimer des énoncés mathématiques, leurs preuves, et vérifier que la preuve prouve bien l'énoncé.
En voici un exemple accessible bsky.app/profile/lips...
En voici un exemple accessible bsky.app/profile/lips...
J'en parlais un peu par ici bsky.app/profile/lips...
Les systèmes utilisés par Google (AlphaGeometry et plus récemment AlphaProof) pour résoudre des problèmes type IMO reposent sur des systèmes formels, ce qui permet de vérifier automatiquement les étapes générées.
AlphaGeometry utilise un langage dédié à la géométrie et AlphaProof utilise Lean.
...
AlphaGeometry utilise un langage dédié à la géométrie et AlphaProof utilise Lean.
...
November 19, 2025 at 3:42 PM
J'en parlais un peu par ici bsky.app/profile/lips...
en l'état actuel des choses ces LLM tout seuls sont incapables de résoudre ce genre de problèmes. D'ailleurs, le LLM tout seul ne sait même pas formaliser les problèmes (ils ont été traduits à la main en Lean dans le cas de AlphaProof).
November 19, 2025 at 3:42 PM
en l'état actuel des choses ces LLM tout seuls sont incapables de résoudre ce genre de problèmes. D'ailleurs, le LLM tout seul ne sait même pas formaliser les problèmes (ils ont été traduits à la main en Lean dans le cas de AlphaProof).
Les systèmes AlphaGeometry (spécialisé en géométrie euclidienne) et AlphaProof (qui traite les problèmes hors géométrie euclidienne) utilisent principalement des systèmes formels, donc une forme d'IA symbolique.
Dans les deux cas, des LLM sont utilisés pour guider la génération de preuves mais,
Dans les deux cas, des LLM sont utilisés pour guider la génération de preuves mais,
November 19, 2025 at 3:42 PM
Les systèmes AlphaGeometry (spécialisé en géométrie euclidienne) et AlphaProof (qui traite les problèmes hors géométrie euclidienne) utilisent principalement des systèmes formels, donc une forme d'IA symbolique.
Dans les deux cas, des LLM sont utilisés pour guider la génération de preuves mais,
Dans les deux cas, des LLM sont utilisés pour guider la génération de preuves mais,
J'ai regardé ta vidéo hier, elle est très bien, ce passage (19:50) m'a cependant interpelé :
> Les LLM d'OpenAI et Google ont chacun remporté la médaille d'or aux Olympiades Internationales de mathématiques.
youtu.be/nqFlQJI6OrE?...
Dit comme ça, c'est faux, et il me semble important de préciser :
> Les LLM d'OpenAI et Google ont chacun remporté la médaille d'or aux Olympiades Internationales de mathématiques.
youtu.be/nqFlQJI6OrE?...
Dit comme ça, c'est faux, et il me semble important de préciser :
L'autonomie des IA expliquée aux humains
YouTube video by Monsieur Phi
youtu.be
November 19, 2025 at 3:42 PM
J'ai regardé ta vidéo hier, elle est très bien, ce passage (19:50) m'a cependant interpelé :
> Les LLM d'OpenAI et Google ont chacun remporté la médaille d'or aux Olympiades Internationales de mathématiques.
youtu.be/nqFlQJI6OrE?...
Dit comme ça, c'est faux, et il me semble important de préciser :
> Les LLM d'OpenAI et Google ont chacun remporté la médaille d'or aux Olympiades Internationales de mathématiques.
youtu.be/nqFlQJI6OrE?...
Dit comme ça, c'est faux, et il me semble important de préciser :