Thomas (lipsum.dev)
@lipsum.dev
Maths et applications, avec les mains et avec du code 💻
https://lipsum.dev
https://lipsum.dev
You might want to have a look at github.com/jrclogic/SMC...
(I proved a version of the blue-eyed islanders puzzle here with it gist.github.com/tchaumeny/fd...)
(I proved a version of the blue-eyed islanders puzzle here with it gist.github.com/tchaumeny/fd...)
GitHub - jrclogic/SMCDEL: A symbolic model checker for Dynamic Epistemic Logic.
A symbolic model checker for Dynamic Epistemic Logic. - jrclogic/SMCDEL
github.com
December 4, 2025 at 11:48 PM
You might want to have a look at github.com/jrclogic/SMC...
(I proved a version of the blue-eyed islanders puzzle here with it gist.github.com/tchaumeny/fd...)
(I proved a version of the blue-eyed islanders puzzle here with it gist.github.com/tchaumeny/fd...)
* Are there other ways (than topos theory) to develop a synthetic approach of mathematics (according to the philosophy presented in the introduction)?
December 3, 2025 at 5:57 PM
* Are there other ways (than topos theory) to develop a synthetic approach of mathematics (according to the philosophy presented in the introduction)?
* Why should topos theory be a natural choice for a synthetic approach of mathematics (it seems obvious from the writer perspective, but it might not be for the reader)?
December 3, 2025 at 5:57 PM
* Why should topos theory be a natural choice for a synthetic approach of mathematics (it seems obvious from the writer perspective, but it might not be for the reader)?
Thanks for taking the time to write about it. Here are my first thoughts after reading this:
* The transition from Euclidean geometry to modern mathematics ("In modern terminology ...") is a abrupt -- I mean the prerequisites to understand what it is talking about change drastically.
* The transition from Euclidean geometry to modern mathematics ("In modern terminology ...") is a abrupt -- I mean the prerequisites to understand what it is talking about change drastically.
December 3, 2025 at 5:57 PM
Thanks for taking the time to write about it. Here are my first thoughts after reading this:
* The transition from Euclidean geometry to modern mathematics ("In modern terminology ...") is a abrupt -- I mean the prerequisites to understand what it is talking about change drastically.
* The transition from Euclidean geometry to modern mathematics ("In modern terminology ...") is a abrupt -- I mean the prerequisites to understand what it is talking about change drastically.
BTW ce petit bouquin est très bien pour une introduction à ce sujet www.cambridge.org/core/books/e...
Emergence and Reduction in Physics
Cambridge Core - Philosophy: General Interest - Emergence and Reduction in Physics
www.cambridge.org
December 2, 2025 at 7:29 PM
BTW ce petit bouquin est très bien pour une introduction à ce sujet www.cambridge.org/core/books/e...
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...