Thomas (lipsum.dev)
@lipsum.dev
📤 73
📥 102
📝 585
Maths et applications, avec les mains et avec du code 💻
https://lipsum.dev
pinned post!
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.
10 months ago
1
13
3
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
1 day 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 🧵⬇️ …
8 days ago
2
2
2
« That's the way modern, you know, logic nerds think it's supposed to be right. » 😲
about 1 month 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
about 2 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 ?
about 2 months ago
1
1
2
reposted by
Thomas (lipsum.dev)
« 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
» ...
loading . . .
AlphaProof Interest Form
Thanks for your interest in AlphaProof. To deliver a reliable user experience, we are carefully managing our compute resources to maintain system stability. We will be reviewing applications and prior...
https://deepmind.google/alphaproof
about 2 months ago
1
0
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.
about 2 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
about 2 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 ∀∃¬∧∨).
about 2 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/
2 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
2 months ago
1
0
0
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
2 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/
2 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
2 months ago
0
0
0
🧐📖 par
@sandradmitchell.bsky.social
2 months ago
0
1
1
La vraie raison du changement de nom de Coq en Rocq...
3 months ago
0
2
0
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).
3 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, ...
3 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.
3 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.
3 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/
3 months ago
0
0
1
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/...
loading . . .
SMCDEL 1.3.0
https://w4eg.de/malvin/illc/smcdelweb/index.html
4 months ago
0
2
2
Au sujet de la blague « Trois logiciens entrent dans un bar » 🧵
4 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.
4 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 :
4 months ago
1
1
2
Il existerait d'autres choses que les maths et l'info dans ce bas monde 🤯 ?
4 months ago
0
0
0
Spot on? (source:
www.reddit.com/r/mathmemes/...
)
4 months ago
1
1
0
Cette image serait-elle fausse !?! ⬇️
7 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/
7 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.
8 months ago
1
6
2
reposted by
Thomas (lipsum.dev)
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
8 months ago
1
2
1
Quand un petit rigolo a emprunté le bouquin avant toi 😅
9 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
10 months ago
1
0
0
reposted by
Thomas (lipsum.dev)
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
10 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
10 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.
10 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/
12 months 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