Thomas🪴
@lipsum.dev
📤 82
📥 130
📝 699
Maths et applications, avec les mains et avec du code 💻
https://blog.lipsum.dev
pinned post!
J'ai enregistré une série de petites vidéos issues de mon apprentissage de Lean et de la théorie des types. J'essaie d'y introduire les concepts par l'exemple plus que par la théorie (j'espère que les experts en théorie des types supporteront mes approximations).
www.youtube.com/playlist?lis...
loading . . .
Lean et théorie des types : une introduction par l'exemple - YouTube
Ces vidéos visent à introduire Lean (https://lean-lang.org/), un langage de programmation fonctionnel qui permet également d'exprimer et démontrer des propos...
https://www.youtube.com/playlist?list=PLtg_rXPiIONQ0PybkWFRoHCI2YS-dmZM7
2 months ago
0
3
2
reposted by
Thomas🪴
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.
about 1 year ago
1
16
7
Prochaine lecture de vacances (par
@romainbrette.bsky.social
)
10 days ago
0
1
0
reposted by
Thomas🪴
Le chapitre 7 du livre *Deep Learning in Science* de Pierre Baldi discute de cette question, à mon sens trop peu abordée dans les débats intelligence naturelle vs artificielle.
www.igb.uci.edu/~pfbaldi/boo...
loading . . .
https://www.igb.uci.edu/~pfbaldi/book-deep-learning-in-science/Ch7-LocalLearnihng.pdf
15 days ago
0
0
2
Est-ce une différence fondamentale (homme / machine) que la "backward propagation", contrairement à l'apprentissage Hebbien, ne respecte pas le principe de localité ?
15 days ago
1
0
0
Question langages de programmation et terminologie : Est-ce que vous traduisez "pattern matching" en français ? Si oui, comment ?
22 days ago
3
2
1
I know a recursive joke, but it's totally WF.
26 days ago
0
0
0
Petits plaisirs saisonniers.
29 days ago
0
0
0
Nouvelle petite vidéo, en préambule à l'induction sur les relations bien-fondées en Lean.
www.youtube.com/watch?v=lEnC...
loading . . .
Fonctions récursives et terminaison [Lean #8]
YouTube video by Lipsum dot dev
https://www.youtube.com/watch?v=lEnCy2qQY4k&list=PLtg_rXPiIONQ0PybkWFRoHCI2YS-dmZM7&index=8
about 1 month ago
0
0
0
Lean et théorie des types : une introduction par l'exemple #7
www.youtube.com/watch?v=H92J...
loading . . .
Type somme, OU logique et principe du tiers exclu [Lean #7]
YouTube video by Lipsum dot dev
https://www.youtube.com/watch?v=H92J3gEIe4I&list=PLtg_rXPiIONQ0PybkWFRoHCI2YS-dmZM7&index=7
about 1 month ago
0
1
0
www.youtube.com/watch?v=2dFz...
loading . . .
Autour du paradoxe de Curry [Lean #6]
YouTube video by Lipsum dot dev
https://www.youtube.com/watch?v=2dFzwEJ9jbI
about 2 months ago
0
1
0
J'ai enregistré une série de petites vidéos issues de mon apprentissage de Lean et de la théorie des types. J'essaie d'y introduire les concepts par l'exemple plus que par la théorie (j'espère que les experts en théorie des types supporteront mes approximations).
www.youtube.com/playlist?lis...
loading . . .
Lean et théorie des types : une introduction par l'exemple - YouTube
Ces vidéos visent à introduire Lean (https://lean-lang.org/), un langage de programmation fonctionnel qui permet également d'exprimer et démontrer des propos...
https://www.youtube.com/playlist?list=PLtg_rXPiIONQ0PybkWFRoHCI2YS-dmZM7
2 months ago
0
3
2
Un nouveau groupe Bourbaki ?
2 months ago
0
1
0
Ce bouquin à paraître a l'air tout à fait prometteur !
link.springer.com/book/9783031...
loading . . .
Proof Assistants and Their Applications in Mathematics and Computer Science
This book is an introduction and reference for topics related to the underlying logical formalisms, architectures, and applications of proof assistants.
https://link.springer.com/book/9783031851896
3 months ago
0
0
0
Où j'essaie d'écraser une mouche avec un marteau...
add a skeleton here at some point
3 months ago
0
1
0
La polarisation des positionnements au sujet de l'IA sur les RS me semble assez extrême : · d'un côté ceux qui ne veulent pas en entendre parler et/ou font comme s'il ne pouvait y avoir aucun usage utile · de l'autre ceux qui reprennent les annonces des OpenAI & co sans aucun regard critique
3 months ago
0
4
1
Quelqu'un saurait pourquoi ce bouquin est devenu introuvable ? (sauf à 788,92€ sur Amazon :-/ )
3 months ago
1
3
1
Tiens il faudrait peut-être que je le (re)lise ❄️
4 months ago
0
0
0
My first real Lean project: a formalization of the Kleene tree🌳
github.com/tchaumeny/Kl...
loading . . .
GitHub - tchaumeny/KleeneTree: Construction of the Kleene tree in Lean
Construction of the Kleene tree in Lean. Contribute to tchaumeny/KleeneTree development by creating an account on GitHub.
https://github.com/tchaumeny/KleeneTree
4 months ago
1
4
2
En ce moment, quand j'ai un peu de temps, j'essaie d'apprendre à coder en Lean. Un petit fil à ce sujet 🧵⬇️ …
4 months ago
2
2
2
« That's the way modern, you know, logic nerds think it's supposed to be right. » 😲
5 months ago
1
1
0
Combien de fois faut-il couper une tablette de chocolat 🍫 de taille a×b pour séparer tous ses carreaux individuellement ?
5 months ago
1
1
1
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.
6 months ago
1
1
0
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 !
add a skeleton here at some point
6 months ago
1
1
0
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 ∀∃¬∧∨).
6 months ago
2
2
2
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
loading . . .
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...
https://neuronaldynamics.epfl.ch/
6 months ago
1
0
0
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 ℝ ?
add a skeleton here at some point
6 months ago
1
0
0
reposted by
Thomas🪴
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
6 months ago
2
2
3
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 ?
loading . . .
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.
https://imperialcollegelondon.github.io/FLT/
6 months ago
1
1
0
🧐📖 par
@sandradmitchell.bsky.social
6 months ago
0
1
1
La vraie raison du changement de nom de Coq en Rocq...
6 months ago
0
2
1
reposted by
Thomas🪴
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).
6 months ago
0
1
1
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, ...
7 months ago
1
2
2
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.
7 months ago
1
1
0
Ci-dessous, une connexion synaptique entre une cellule nerveuse et une cellule musculaire. On peut distinguer en haut deux vésicules contenant des neurotransmetteurs.
7 months ago
1
0
0
Nouvel article sur mon blog !
lipsum.dev/2025-09-1-en...
loading . . .
Blague, énigme et raisonnement automatisé
Dans un article du journal Le Monde , le vulgarisateur Mickaël Launay présente la blague suivante : C'est l'histoire de trois logiciennes qui entrent dans un…
https://lipsum.dev/2025-09-1-enigme-logique-epistemique/
7 months ago
0
0
1
reposted by
Thomas🪴
In case anyone has doubts about the validity of the joke, note that it has been formally proven in
w4eg.de/malvin/illc/...
loading . . .
SMCDEL 1.3.0
https://w4eg.de/malvin/illc/smcdelweb/index.html
7 months ago
0
2
2
Au sujet de la blague « Trois logiciens entrent dans un bar » 🧵
7 months ago
1
0
1
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.
8 months ago
1
3
0
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 :
8 months ago
1
1
2
Il existerait d'autres choses que les maths et l'info dans ce bas monde 🤯 ?
8 months ago
0
0
0
Spot on? (source:
www.reddit.com/r/mathmemes/...
)
8 months ago
1
1
0
Cette image serait-elle fausse !?! ⬇️
11 months ago
1
2
2
« À 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...
loading . . .
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…
https://lipsum.dev/2025-05-1-impossible-informatique-theorique/
11 months ago
1
3
1
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.
12 months ago
1
6
2
reposted by
Thomas🪴
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/...
.
loading . . .
Neural networks and physical systems with emergent collective computational abilities. | PNAS
Computational properties of use of biological organisms or to the construction of computers can emerge as collective properties of systems having a...
https://www.pnas.org/doi/10.1073/pnas.79.8.2554
12 months ago
1
2
1
Quand un petit rigolo a emprunté le bouquin avant toi 😅
about 1 year ago
0
1
0
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.
loading . . .
How to verify your Bluesky account - Bluesky
Here's how to verify your Bluesky account by setting your website as your username.
https://bsky.social/about/blog/4-28-2023-domain-handle-tutorial
about 1 year ago
1
0
0
reposted by
Thomas🪴
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.
loading . . .
https://github.com/python/cpython/blob/main/Objects/listobject.c#L1488
about 1 year ago
1
1
1
Interview très intéressante de N. Schaeffer par
@scienceetonnante.com
, qui parle notamment de la transformée en harmoniques sphériques.
add a skeleton here at some point
about 1 year ago
1
1
0
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.
about 1 year ago
1
16
7
Load more
feeds!
log in