Thomas🪴
@lipsum.dev
📤 80
📥 116
📝 644
Maths et applications, avec les mains et avec du code 💻
https://blog.lipsum.dev
pinned post!
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
about 2 months ago
1
4
2
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 18 hours 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
4 days ago
0
3
2
Un nouveau groupe Bourbaki ?
10 days ago
0
1
0
reposted by
Thomas🪴
Et pourtant, si j'en crois
www.cambridge.org/core/element...
que je viens de lire, les scientifiques ont du mal à s'affranchir des jugements de valeur (et donc des opinions). Moi mon opinion au doigt mouillé c'est que beaucoup de questions scientifiques sont extrêmement politisées (notamment du...
loading . . .
Values in Science
Cambridge Core - Philosophy: General Interest - Values in Science
https://www.cambridge.org/core/elements/abs/values-in-science/8C9899A25764AA9A791287325A511C3C
15 days ago
1
0
1
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
29 days ago
0
0
0
Le paradoxe de ... ? ```lean example : (P ↔ (P → Q)) → Q := fun h => h.1 (h.2 fun p => h.1 p p) (h.2 fun p => h.1 p p) ```
29 days ago
0
0
0
Où j'essaie d'écraser une mouche avec un marteau...
add a skeleton here at some point
about 1 month 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
about 1 month ago
0
4
1
Quelqu'un saurait pourquoi ce bouquin est devenu introuvable ? (sauf à 788,92€ sur Amazon :-/ )
about 2 months ago
1
3
1
Tiens il faudrait peut-être que je le (re)lise ❄️
about 2 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
about 2 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 🧵⬇️ …
2 months ago
2
2
2
« That's the way modern, you know, logic nerds think it's supposed to be right. » 😲
3 months ago
1
1
0
Bonne réponse de
@roger-mansuy.bsky.social
! Saviez-vous que l'on peut démontrer informatiquement ce type de résultat ?
add a skeleton here at some point
3 months ago
1
0
0
Combien de fois faut-il couper une tablette de chocolat 🍫 de taille a×b pour séparer tous ses carreaux individuellement ?
3 months ago
1
1
2
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.
4 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
4 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 ∀∃¬∧∨).
4 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/
4 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
4 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
4 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/
4 months ago
1
1
0
Est-ce que quelqu'un aurait des ressources à suggérer concernant la machine de Cox-Zucker ?
en.wikipedia.org/wiki/Cox%E2%...
loading . . .
Cox–Zucker machine - Wikipedia
https://en.wikipedia.org/wiki/Cox%E2%80%93Zucker_machine
4 months ago
0
0
0
🧐📖 par
@sandradmitchell.bsky.social
4 months ago
0
1
1
La vraie raison du changement de nom de Coq en Rocq...
4 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).
5 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, ...
5 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.
5 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.
5 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/
5 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
6 months ago
0
2
2
Au sujet de la blague « Trois logiciens entrent dans un bar » 🧵
6 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.
6 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 :
6 months ago
1
1
2
Il existerait d'autres choses que les maths et l'info dans ce bas monde 🤯 ?
6 months ago
0
0
0
Spot on? (source:
www.reddit.com/r/mathmemes/...
)
6 months ago
1
1
0
Cette image serait-elle fausse !?! ⬇️
9 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/
9 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.
10 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
10 months ago
1
2
1
Quand un petit rigolo a emprunté le bouquin avant toi 😅
11 months 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
12 months 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
12 months 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
12 months 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.
12 months ago
1
13
3
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...
loading . . .
Satisfaisabilité, frustration et transitions de phase
Vous êtes chargé des invitations pour une grande fête familiale, mais vos proches vous ont imposé certaines conditions : Votre mère vous demande d'inviter…
https://lipsum.dev/2025-01-1-sat-frustration/
about 1 year ago
2
5
0
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...
loading . . .
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…
https://lipsum.dev/2024-07-1-mecanisation-geometrie/
about 1 year ago
0
3
0
you reached the end!!
feeds!
log in