Thomas (lipsum.dev)
@lipsum.dev
Maths et applications, avec les mains et avec du code 💻
https://lipsum.dev
https://lipsum.dev
Pinned
Thomas (lipsum.dev)
@lipsum.dev
· Mar 15
Un petit fil pour parler du modèle d'Ising et de ses simulations informatiques ⬇️
Sujet à l'intersection de la physique statistique, de l'algorithmique et des probabilités.
Sujet à l'intersection de la physique statistique, de l'algorithmique et des probabilités.
Reposted by Thomas (lipsum.dev)
Cet article qui vient de sortir semble présenter le fonctionnement d'un logiciel, AlphaProof, (qui serait) capable de générer des preuves de problèmes type IMO en Lean.
Pas encore eu le temps de le lire, à suivre...
www.nature.com/articles/s41...
Pas encore eu le temps de le lire, à suivre...
www.nature.com/articles/s41...
Olympiad-level formal mathematical reasoning with reinforcement learning - Nature
Nature - Olympiad-level formal mathematical reasoning with reinforcement learning
www.nature.com
November 12, 2025 at 10:34 PM
Cet article qui vient de sortir semble présenter le fonctionnement d'un logiciel, AlphaProof, (qui serait) capable de générer des preuves de problèmes type IMO en Lean.
Pas encore eu le temps de le lire, à suivre...
www.nature.com/articles/s41...
Pas encore eu le temps de le lire, à suivre...
www.nature.com/articles/s41...
Belle illustration de la formule d'Euler au musée du Compagnonnage à Tours, avec ce ballon en bois conçu à partir de 12 pentagones et 20 hexagones.
November 10, 2025 at 4:47 PM
Belle illustration de la formule d'Euler au musée du Compagnonnage à Tours, avec ce ballon en bois conçu à partir de 12 pentagones et 20 hexagones.
La magie d'internet : je partage innocemment un petit problème que j'avais découvert par hasard, et j'en apprends une autre solution par quelqu'un qui a justement écrit un papier sur un algorithme qui permet de prouver (un lemme menant vers) le résultat !
Oui. :)
November 5, 2025 at 8:48 PM
La magie d'internet : je partage innocemment un petit problème que j'avais découvert par hasard, et j'en apprends une autre solution par quelqu'un qui a justement écrit un papier sur un algorithme qui permet de prouver (un lemme menant vers) le résultat !
Un problème de mathématiques / logique que j'ai trouvé intéressant ⬇️
Montrer qu'il est impossible de définir la multiplication des nombres réels à partir des opérations + et - (et des symboles logiques ∀∃¬∧∨).
Montrer qu'il est impossible de définir la multiplication des nombres réels à partir des opérations + et - (et des symboles logiques ∀∃¬∧∨).
November 4, 2025 at 7:59 PM
Un problème de mathématiques / logique que j'ai trouvé intéressant ⬇️
Montrer qu'il est impossible de définir la multiplication des nombres réels à partir des opérations + et - (et des symboles logiques ∀∃¬∧∨).
Montrer qu'il est impossible de définir la multiplication des nombres réels à partir des opérations + et - (et des symboles logiques ∀∃¬∧∨).
Retour sur deux livres autour des neurosciences computationnelles — qui cherchent notamment à établir des modèles mathématiques de l'activité neuronale.
Le premier, *Neuronal Dynamics: From single neurons to networks and models of cognition* est disponible en ligne neuronaldynamics.epfl.ch
Le premier, *Neuronal Dynamics: From single neurons to networks and models of cognition* est disponible en ligne neuronaldynamics.epfl.ch
Neuronal Dynamics - a neuroscience textbook by Wulfram Gerstner, Werner M. Kistler, Richard Naud and Liam Paninski
Homepage of the computational neuroscience book "Neuronal Dynamics" written by Wulfram Gerstner, Werner M. Kistler, Richard Naud and Liam Paninski. Visit us for the free online book, teaching material...
neuronaldynamics.epfl.ch
November 1, 2025 at 5:38 PM
Retour sur deux livres autour des neurosciences computationnelles — qui cherchent notamment à établir des modèles mathématiques de l'activité neuronale.
Le premier, *Neuronal Dynamics: From single neurons to networks and models of cognition* est disponible en ligne neuronaldynamics.epfl.ch
Le premier, *Neuronal Dynamics: From single neurons to networks and models of cognition* est disponible en ligne neuronaldynamics.epfl.ch
Je n'ai pas lu le détail, mais une question me titille : si ces résultats sont démontrés en utilisant des nombres réels (comme le suggère l'image), dans quelle mesure s'appliquent-ils aux algorithmes utilisés dans la vraie vie, sachant qu'un ordinateur ne connaît pas ℝ ?
LLMs are injective and invertible.
They show that different prompts always map to different embeddings, and this property can be used to recover input tokens from individual embeddings in latent space.
Paper: www.arxiv.org/abs/2510.15511
They show that different prompts always map to different embeddings, and this property can be used to recover input tokens from individual embeddings in latent space.
Paper: www.arxiv.org/abs/2510.15511
October 30, 2025 at 8:36 PM
Je n'ai pas lu le détail, mais une question me titille : si ces résultats sont démontrés en utilisant des nombres réels (comme le suggère l'image), dans quelle mesure s'appliquent-ils aux algorithmes utilisés dans la vraie vie, sachant qu'un ordinateur ne connaît pas ℝ ?
Reposted by Thomas (lipsum.dev)
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
October 29, 2025 at 4:18 PM
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
Il y a un projet de formalisation en Lean du grand théorème de Fermat et ceux qui bossent dessus ne sont pas sûrs de le finaliser avant plusieurs années : imperialcollegelondon.github.io/FLT/
Comment réconcilier cela avec les prouesses que l'on prête aux IA en termes de formalisation automatique ?
Comment réconcilier cela avec les prouesses que l'on prête aux IA en termes de formalisation automatique ?
Fermat’s Last Theorem
An ongoing multi-author open source project to formalise a proof of Fermat’s Last Theorem in the Lean theorem prover.
imperialcollegelondon.github.io
October 27, 2025 at 8:57 PM
Il y a un projet de formalisation en Lean du grand théorème de Fermat et ceux qui bossent dessus ne sont pas sûrs de le finaliser avant plusieurs années : imperialcollegelondon.github.io/FLT/
Comment réconcilier cela avec les prouesses que l'on prête aux IA en termes de formalisation automatique ?
Comment réconcilier cela avec les prouesses que l'on prête aux IA en termes de formalisation automatique ?
Est-ce que quelqu'un aurait des ressources à suggérer concernant la machine de Cox-Zucker ?
en.wikipedia.org/wiki/Cox%E2%...
en.wikipedia.org/wiki/Cox%E2%...
Cox–Zucker machine - Wikipedia
en.wikipedia.org
October 20, 2025 at 5:24 PM
Est-ce que quelqu'un aurait des ressources à suggérer concernant la machine de Cox-Zucker ?
en.wikipedia.org/wiki/Cox%E2%...
en.wikipedia.org/wiki/Cox%E2%...
La vraie raison du changement de nom de Coq en Rocq...
October 18, 2025 at 11:31 AM
La vraie raison du changement de nom de Coq en Rocq...
Reposted by Thomas (lipsum.dev)
mais aussi pour le débat public et la science qui ne souffrira pas trop du cherry-picking inhérent à toute volonté d'appuyer des décisions *politiques* sur une "autorité scientifique" (sur ce point, mon propos serait le même concernant des sujets économiques d'actualité d'ailleurs).
October 15, 2025 at 9:08 AM
mais aussi pour le débat public et la science qui ne souffrira pas trop du cherry-picking inhérent à toute volonté d'appuyer des décisions *politiques* sur une "autorité scientifique" (sur ce point, mon propos serait le même concernant des sujets économiques d'actualité d'ailleurs).
L’Analyse en Composantes Principales
—
Leur système politique était au bord de l’implosion et ils le savaient. Mais ils avaient un plan.
Le supercalculateur venait d’achever la diagonalisation de la gigantesque matrice des idées, ...
—
Leur système politique était au bord de l’implosion et ils le savaient. Mais ils avaient un plan.
Le supercalculateur venait d’achever la diagonalisation de la gigantesque matrice des idées, ...
October 10, 2025 at 5:32 PM
L’Analyse en Composantes Principales
—
Leur système politique était au bord de l’implosion et ils le savaient. Mais ils avaient un plan.
Le supercalculateur venait d’achever la diagonalisation de la gigantesque matrice des idées, ...
—
Leur système politique était au bord de l’implosion et ils le savaient. Mais ils avaient un plan.
Le supercalculateur venait d’achever la diagonalisation de la gigantesque matrice des idées, ...
Deux livres que je recommande vivement, pour celles et ceux qui souhaiteraient s'initier à des thèmes mathématiques proches de la logique et de l'informatique théorique.
October 1, 2025 at 7:37 PM
Deux livres que je recommande vivement, pour celles et ceux qui souhaiteraient s'initier à des thèmes mathématiques proches de la logique et de l'informatique théorique.
Ci-dessous, une connexion synaptique entre une cellule nerveuse et une cellule musculaire. On peut distinguer en haut deux vésicules contenant des neurotransmetteurs.
![Source : https://ccsb.scripps.edu/goodsell/machinery-of-life-reducedillustrations/#iLightbox[gallery_image_1]/52](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:denld7ao24tcahogbclo3if3/bafkreiatobr37qiphhhw265tu2bzmpc5xaunsxauhwrb6op5n5teehbfxa@jpeg)
September 27, 2025 at 7:34 AM
Ci-dessous, une connexion synaptique entre une cellule nerveuse et une cellule musculaire. On peut distinguer en haut deux vésicules contenant des neurotransmetteurs.
Reposted by Thomas (lipsum.dev)
In case anyone has doubts about the validity of the joke, note that it has been formally proven in w4eg.de/malvin/illc/...
SMCDEL 1.3.0
w4eg.de
September 15, 2025 at 7:48 AM
In case anyone has doubts about the validity of the joke, note that it has been formally proven in w4eg.de/malvin/illc/...
Au sujet de la blague « Trois logiciens entrent dans un bar » 🧵
September 15, 2025 at 7:47 AM
Au sujet de la blague « Trois logiciens entrent dans un bar » 🧵
Implémentation de la projection Mercator dans la bibliothèque Leaflet leafletjs.com.
Ci-dessous, le code (JavaScript) de la projection associée à des coordonnées ellipsoïdales.
Ci-dessous, le code (JavaScript) de la projection associée à des coordonnées ellipsoïdales.
September 12, 2025 at 11:11 AM
Implémentation de la projection Mercator dans la bibliothèque Leaflet leafletjs.com.
Ci-dessous, le code (JavaScript) de la projection associée à des coordonnées ellipsoïdales.
Ci-dessous, le code (JavaScript) de la projection associée à des coordonnées ellipsoïdales.
Dans « Essai d’une théorie algébrique des nombres entiers, précédé d'une introduction logique à une théorie déductive quelconque », Alessandro Padoa décrit informellement, en 1901, la démarche qui mènera à la logique moderne :
August 30, 2025 at 11:07 AM
Dans « Essai d’une théorie algébrique des nombres entiers, précédé d'une introduction logique à une théorie déductive quelconque », Alessandro Padoa décrit informellement, en 1901, la démarche qui mènera à la logique moderne :
Il existerait d'autres choses que les maths et l'info dans ce bas monde 🤯 ?
August 27, 2025 at 1:45 PM
Il existerait d'autres choses que les maths et l'info dans ce bas monde 🤯 ?
August 24, 2025 at 6:57 AM
Cette image serait-elle fausse !?! ⬇️
June 10, 2025 at 7:58 PM
Cette image serait-elle fausse !?! ⬇️
« À l'impossible nul n'est tenu. »
J'ai écrit un article de blog pour détailler un peu la résolution d'un problème d'informatique que j'ai partagé ici il y a quelques semaines.
lipsum.dev/2025-05-1-im...
J'ai écrit un article de blog pour détailler un peu la résolution d'un problème d'informatique que j'ai partagé ici il y a quelques semaines.
lipsum.dev/2025-05-1-im...
Sur un résultat d'impossibilité en informatique
Considérons le problème algorithmique suivant : On représente un nombre réel par un programme en Python qui énumère les chiffres de sa représentation décimale…
lipsum.dev
May 31, 2025 at 6:56 AM
« À l'impossible nul n'est tenu. »
J'ai écrit un article de blog pour détailler un peu la résolution d'un problème d'informatique que j'ai partagé ici il y a quelques semaines.
lipsum.dev/2025-05-1-im...
J'ai écrit un article de blog pour détailler un peu la résolution d'un problème d'informatique que j'ai partagé ici il y a quelques semaines.
lipsum.dev/2025-05-1-im...
Petit problème d'informatique que j'ai trouvé intéressant :
On encode des nombres réels sous la forme de programmes (disons, en Python par ex.) qui énumèrent leurs développements décimaux.
On encode des nombres réels sous la forme de programmes (disons, en Python par ex.) qui énumèrent leurs développements décimaux.
May 8, 2025 at 11:26 AM
Petit problème d'informatique que j'ai trouvé intéressant :
On encode des nombres réels sous la forme de programmes (disons, en Python par ex.) qui énumèrent leurs développements décimaux.
On encode des nombres réels sous la forme de programmes (disons, en Python par ex.) qui énumèrent leurs développements décimaux.