My first real Lean project: a formalization of the Kleene tree🌳 github.com/tchaumeny/Kl...

En ce moment, quand j'ai un peu de temps, j'essaie d'apprendre à coder en Lean. Un petit fil à ce sujet 🧵⬇️ …

« That's the way modern, you know, logic nerds think it's supposed to be right. » 😲

Bonne réponse de @roger-mansuy.bsky.social ! Saviez-vous que l'on peut démontrer informatiquement ce type de résultat ?

Combien de fois faut-il couper une tablette de chocolat 🍫 de taille a×b pour séparer tous ses carreaux individuellement ?

« We are making AlphaProof’s capabilities available to members of the scientific community through an interactive tool communicating with Google servers. Researchers interested in gaining access will be able to apply at deepmind.google/alphaproof » ...

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 !

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 ∀∃¬∧∨).

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

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 ℝ ?

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

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 ?

Est-ce que quelqu'un aurait des ressources à suggérer concernant la machine de Cox-Zucker ? en.wikipedia.org/wiki/Cox%E2%...

🧐📖 par @sandradmitchell.bsky.social

La vraie raison du changement de nom de Coq en Rocq...

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, ...

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.

Nouvel article sur mon blog ! lipsum.dev/2025-09-1-en...

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 » 🧵

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.

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 🤯 ?

Spot on? (source: www.reddit.com/r/mathmemes/...)

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...

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.

Par exemple, le prix de Nobel de physique 2024 a été attribué à John Hopfield, essentiellement pour son papier sur les réseaux de neurones qui portent son nom www.pnas.org/doi/10.1073/....

Quand un petit rigolo a emprunté le bouquin avant toi 😅

As described in bsky.social/about/blog/4..., if you own a domain, you can use it as a custom handle (e.g. lipsum.dev in my case). Beware when doing this, as links using the previous handle (e.g. links to your posts, previously shared outside) are NOT redirected and will show an error.

Par exemple dans le cas d'une liste L = [1, 2, 3], écrire L += [4, 5, 6] n'est pas équivalent du point de vue de l'exécution à L = L + [4, 5, 6] car les listes implémentent la concaténation « in place » (cf github.com/python/cpyth...) pour optimiser le traitement.

Interview très intéressante de N. Schaeffer par @scienceetonnante.com, qui parle notamment de la transformée en harmoniques sphériques.

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.

Sur le problème de la satisfaisabilité booléenne, les transitions de phase associées, et le lien avec des problèmes physiques. lipsum.dev/2025-01-1-sa...

Trois petites histoires autour de thème de l'automatisation du raisonnement géométrique : * L'axiome de Pasch et les limites de la géométrie d'Euclide * Les preuves informatisées avec l'exemple de GeoCoq * AlphaGeometry et le raisonnement « neuro-symbolique » lipsum.dev/2024-07-1-me...