Thomas🪴

@lipsum.dev

104 Followers 155 Following

Maths et applications, avec les mains et avec du code 💻 https://blog.lipsum.dev

Capture d'écran des instructions à Mistral vibe : --- In this folder, you will find a file v0.lean with the current implementation of the proof of excluded-middle (`theorem em (p : Prop) : p ∨ ¬p`) in Lean 4. When running this we see that it depends on the axiom `Quot.sound`, which is introduced through the usage of `funext`: $ lean v0.lean 'em' depends on axioms: [propext, Classical.choice, Quot.sound] I would like you to refactor this proof so that it does *not* use `funext` and the axiom `Quot.sound`. One way to do this is by using a boolean `b : Bool` instead of `x : Prop` (you can already change it in the current version) and simply encoding U and V as the pairs of propositions `(⊤,P)` and `(P,⊤)` instead of functions. Write your implementation in a file v1.lean and check that it no longer depends on `Quot.sound`.
Summary I have successfully implemented the computability theorem that proves there is no computable function that can separate programs returning 0 from those returning a nonzero result (with the function being able to take any value when the program does not terminate). Implementation Details The theorem is proved in /workspace/myproject/Separation.lean using the following approach: 1. Theorem Statement: The main theorem no_computable_separation states that there is no computable function f : Code → Bool such that: • If program c halts on input 0 with output 0, then f c = true • If program c halts on input 0 with output ≠ 0, then f c = false • If program c does not halt on input 0, then f c can be either value 2. Proof Strategy: The proof uses Kleene's second recursion theorem (the fixed point theorem) to construct a self-referential program that leads to a contradiction. 3. Key Steps: • Assume such a computable function f exists • Define a partial recursive function h that, given a code c and input n, returns some 1 if f c = true and some 0 if f c = false • By the fixed point theorem, there exists a code e such that eval e = h e • This means eval e 0 = some (bif f e then 1 else 0) • Case 1: If f e = true, then eval e 0 = some 1, so e returns nonzero, but then f e should be false by the assumption on f. Contradiction. • Case 2: If f e = false, then eval e 0 = some 0, so e returns 0, but then f e should be true by the assumption on f. Contradiction. 4. Dependencies: The proof uses: • Mathlib.Computability.Halting for Rice's theorem (though we don't use it directly) • Mathlib.Computability.PartrecCode for the fixed point theorem • Computable.cond for showing that conditional functions are computable • fixed_point₂ (Kleene's second recursion theorem) The implementation is complete and compiles successfully with Mathlib.
Capture d'écran de vibe, j'ai demandé : > Can you create a new Lean file with a proof of the excluded middle principle from Peirce law? Do not use classical axioms of course. Vibe affiche une preuve de ce résultat en Lean accompagnée d'une démonstration informelle (en anglais).
Photographie de la couverture du livre https://press.princeton.edu/books/paperback/9780691281384/the-brain-in-theory
Photo d'un cerisier en fleur, Square du Docteur Calmette à Paris 15ème.
La théorie des ensembles - Patrick Dehornoy
La petite histoire des flocons de neige - Étienne Ghys https://www.odilejacob.fr/catalogue/sciences/physique-chimie/petite-histoire-des-flocons-de-neige_9782738154415.php
Capture d'écran d'une vidéo dans laquelle un intervenant dit : « That's the way modern, you know, logic nerds think it's supposed to be right. »
Photographie d'un ballon de football en bois, au musée du Compagnonnage de Tours.
Photographie de la couverture du livre *Unsimple Truths: Science, Complexity and Policy* par Sandra D. Mitchell
Recherche Google pour « coq type »... on voit des coqs.
Photo des deux livres sur une table : - Hilbert's Tenth Problem (AMS) - Reverse Mathematics (Princeton)
Capture d'écran du tweet https://x.com/gabriel_zucman/status/1969486697525047473 de Gabriel Zucman
Source : https://ccsb.scripps.edu/goodsell/machinery-of-life-reducedillustrations/#iLightbox[gallery_image_1]/52
ChatGPT screenshot Q: What is an anti-anti-anti-anti-anti-anti-anti-anti-fascist? A: We’re stacking the prefix “anti-” (against) in front of “fascist”, and then repeating it eight times: Fascist → someone who supports fascism. Anti-fascist → someone against fascists (e.g., Antifa). Anti-anti-fascist → someone against anti-fascists (which often means they sympathize with fascists or oppose anti-fascist activism). Anti-anti-anti-fascist → someone against those people (so they’re back to being against fascists again). Notice the pattern: Odd numbers of “anti-” → against fascists. Even numbers of “anti-” → against anti-fascists (so, indirectly pro-fascist or at least opposing anti-fascists). Now, with 8 “anti-”s: 8 is even. That means: an anti-anti-anti-anti-anti-anti-anti-anti-fascist is against anti-fascists, i.e. basically the same as an anti-anti-fascist. So the answer is: 👉 An anti-anti-anti-anti-anti-anti-anti-anti-fascist = someone opposed to anti-fascists (thus in a position that aligns with or defends fascists, at least rhetorically).
Formule de "Dynamic Epistemic Logic" associée à la blague des logiciens, cf https://w4eg.de/malvin/illc/smcdelweb/index.html
Capture d'écran de https://www.amazon.fr/-/en/Christian-Leruste/dp/2916352538/, le livre de Topologie Algébrique est vendu 2000€ d'occasion.
Extrait du code source de la projection Mercator (sphérique) de Leaftlet Cf https://github.com/Leaflet/Leaflet/blob/0eee3776d3a6929aad71c2fa112bc4a935b0950c/src/geo/projection/Projection.SphericalMercator.js
Extrait du code source de la projection Mercator (ellipsoïdale) de Leaftlet Cf https://github.com/Leaflet/Leaflet/blob/0eee3776d3a6929aad71c2fa112bc4a935b0950c/src/geo/projection/Projection.Mercator.js
Quatre livres de la collection "A Very Short Introduction" (Oxford) : - The Cell - Philosophy of Biology - Molecular Biology - Agriculture
Photo des 4 dés intransitifs de Bradley Efron (à l'Institut Henri Poincaré)
Image de Han Solo et Chewbacca passant en vitesse lumière à bord du Faucon Millenium. Les étoiles semblent s'écarter les unes des autres.
Image de la sphère de Poincaré illustrant une transformation de Möbius faisant converger les points vers le pôle nord.
Image de Han Solo et Chewbacca passant en vitesse lumière à bord du Faucon Millenium.
Pierre tombale marquée du nom d'Albert Camus, au cimetière de Lourmarin. À côté, des gens ont déposé en hommage des stylos dans un petit pot. La tombe est assez sobre, il n'y a que cette pierre et le reste est de la terre sur laquelle pousse un grand laurier.
Simulation du modèle d'Ising sur un réseau 2500x2500 autour du régime critique.
Histogrammes de la magnétisation sur un réseau 100x100 pour des valeurs de la température correspondant à une plage restreinte autour du régime critique, simulations via l'algorithme de Wolff. On observe en abaissant la température (de gauche à droite sur la première puis la seconde ligne) dans la plage 0.42 ≤ β ≤ 0.45 que le système passe d'une magnétisation totale presque sûrement nulle à une magnétisation presque sûrement totalement positive ou totalement négative.
Représentation de deux états correspondant à une transition a → b par retournement d'un cluster, comme décrit dans l'algorithme de Wolff. Source : https://arxiv.org/abs/cond-mat/0311623
Histogrammes de la magnétisation sur un réseau 4x4 pour différentes valeurs de la température. En abscisse : la valeur de la magnétisation totale (de -16 à +16 unités) En ordonnée : le nombre d'occurrences de cette valeur La « température inverse » β = 1/(kT) augmente progressivement de gauche à droite sur la première puis la seconde ligne.
Représentation d'un réseau carré de type Ising avec des aimants en position "up" (rouge) et "down" (bleu). Source : https://arxiv.org/abs/1903.11554
Courbe représentant la magnétisation en fonction de la température. Source : Lectures On Phase Transitions And The Renormalization Group, N. Goldenfeld.
Simulation du modèle d'Ising sur un réseau 2500x2500 autour du régime critique.