Thomas🪴
@lipsum.dev
Maths et applications, avec les mains et avec du code 💻 https://blog.lipsum.dev
J'essayais d'apprendre des choses sur les sémantiques dénotationnelles du lambda-calcul avec Claude et, rapidement, je me rends compte qu'il me raconte n'importe quoi; ce qu'il finit par remarquer après que je l'ai mis devant sa contradiction.
Je me demande quel est le ratio moyen entre la taille des définitions nécessaires à l'énonciation d'une proposition et la taille de la preuve; en particulier dans le cadre des preuves formalisées. Un cas extrême :
Unpopular opinion: sur le sujet du *réchauffement climatique*, il me semble problématique que les simulations basées sur les modèles de circulation générale soient autant mises en avant, et qu'on parle aussi peu des données satellites sur le spectre d'émission infrarouge sortant de l'atmosphère :
J'ai proposé une pull request dans Lean pour modifier la preuve du principe du tiers-exclu github.com/leanprover/l.... Voyons de quoi il s'agit :
refactor: remove funext dependency from Classical.em, drop Quot.sound by tchaumeny · Pull Request #14420 · leanprover/lean4
This PR removes the usage of funext in the proof of excluded-middle (Diaconescu's theorem). As a result, the dependency on the axiom Quot.sound disappears from em. This small refactoring is ins...
github.com
J'ai testé Leanstral (mistral.ai/news/leanstr...), le modèle de Mistral entraîné spécialement pour Lean, petit compte-rendu : ⬇️
Début d'une petite série de vidéos📹 sur la calculabilité. Le but est d'introduire les concepts généraux, de façon plus rigoureuse que la vulgarisation, mais plus informelle qu'un vrai cours, puis de les illustrer grâce à Lean. www.youtube.com/watch?v=-ym5...
Modèles de calcul, fonctions récursives générales [Introduction à la calculabilité 1]
YouTube video by Lipsum dot dev
youtube.com
Nouvelle vidéo, dans laquelle je parle de programmation fonctionnelle en Lean et d'une monade qui permet de prouver des résultats de complexité algorithmique (avec CSLib). www.youtube.com/watch?v=ak-j...
Programmation fonctionnelle, monades et preuves de complexité [Lean #10]
YouTube video by Lipsum dot dev
youtube.com
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...
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…
lipsum.dev
👨💻▶️ Implémentation interactive ET certification d'un algorithme de tri (quicksort) avec Lean. www.youtube.com/watch?v=RmZy...
Preuve formelle d'un algorithme de tri [Lean #9]
YouTube video by Lipsum dot dev
youtube.com
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.
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...
igb.uci.edu
Est-ce une différence fondamentale (homme / machine) que la "backward propagation", contrairement à l'apprentissage Hebbien, ne respecte pas le principe de localité ?
Question langages de programmation et terminologie : Est-ce que vous traduisez "pattern matching" en français ? Si oui, comment ?
Lean et théorie des types : une introduction par l'exemple #7 www.youtube.com/watch?v=H92J...
Type somme, OU logique et principe du tiers exclu [Lean #7]
YouTube video by Lipsum dot dev
youtube.com
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...
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...
youtube.com
Ce bouquin à paraître a l'air tout à fait prometteur ! link.springer.com/book/9783031...
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.
link.springer.com
Où j'essaie d'écraser une mouche avec un marteau...
Thomas🪴@lipsum.dev · 7mo ago```python from z3 import * s = Solver() m = Int('m') k = Int('k') r = Int('r') X = Int('X') s.add(m >= 0, k >= 0, r >= 0, r < 10, X >= 0) s.add(m*m == (2*k + 1)*10 + r) s.add((k + 1) * 10 - X == k * 10 + r + X) if s.check() == sat: print(s.model()) ``` [r = 6, k = 28, X = 2, m = 24]
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
Quelqu'un saurait pourquoi ce bouquin est devenu introuvable ? (sauf à 788,92€ sur Amazon :-/ )
My first real Lean project: a formalization of the Kleene tree🌳 github.com/tchaumeny/Kl...
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.
github.com
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. » 😲
