6 octobre 2024 ⋅ Retour à l'accueil du blog
Allez savoir pourquoi, je ressens un curieux besoin de rire un peu ces derniers jours.0 D'où l'idée de cette modeste liste d'extraits amusants d'articles ou livres (plus ou moins) scientifiques collectés en quelques mois. N'hésitez pas à proposer vos ajouts !
Ah, la recherche ! Du temps perdu.
— Jean-François Mestre, René Schoof, Lawrence Washington et Don Zagier, Quotients Homophones des Groupes Libres
Stephen Kleene recounts† that he figured out how to compute predecessors while at a dentist's office. Is programming the untyped 𝜆-calculus like pulling one's teeth out?
† Stephen C. Kleene. “Origins of Recursive Function Theory”. In: IEEE Annals of the History of Computing 3 (1981), pp. 52–67
— Andrej Bauer, Notes on realizability
The choice of good terminology, it is too often forgotten, requires a bit of literary talent. Such talent is not displayed by calling a terminal object a ‘terminator’.
— Jaap van Osten, Realizability: An Introduction to its Categorical Side
Zero-content proof techniques
— David Madore, Perfect Localized Security of the Fourtytwofish Cipher in the Delphic Oracle Model (explication pour les non-initiés)
A word about the meta-theory is in order. This article, like almost all in mathematics, is intended to be within classical mathematics. This would be unremarkable, except that it is at the same time an article about constructive mathematics. Just as we are more upset when religious leaders engage in even common sexual transgressions than when lay people do, because we hold them to a higher standard, so are people who discuss constructive mathematics questioned about their use of Excluded Middle when almost everyone else does so without even noticing it.
— Robert Lubarsky, On the failure of BD-ℕ and BD, and an application to the anti-specker property (trouvé par David Madore)
The problem is not P. This problem would not be P, because when using the game ”Debilanda”, in order to get a right answer, the problem puts as a condition the generation of a Turing Machine inside the game ”Debilandia”, for this reason, this problem is reducible to the ”halting problem”, proposed by Turing, who proved that Turing machines and precisely that the halting problem was undecidable [6]. So, since the problem proposed in this article can be reduced to the ”halting problem”, it is also undecidable. […]
the problem is NP. […]
— Daniel Cardona Delgado, P not equal to NP
Regarding the main concerns on the assumption behind Lemma 3.1, we want to clarify that the only approach for exact solutions of CSPs and combinatorial problems is combinatorial search through the solution space. CSPs are analogous to combinatorial problems, for which the current solution methods involve a combinatorial search through the solution space. This is an established and inescapable reality of solving such problems . Combinatorial searches represent the state-of-the-art in precisely solving general CSPs and combinatorial problems, and the current literature does not offer any alternative that escapes the necessity of exploring the search space to find exact solutions. There are infinitely many algorithms that may emerge in the future, and it is impossible to exhaustively enumerate all of them. Regarding these potential future algorithms, it is inevitable to make assumptions that are consistent with the realities. For example, without the Church-Turing thesis, the halting problem cannot be proved to be uncomputable in any machines. Therefore, we wish to clarify that the divide-and-conquer strategy in Lemma 3.1 does not pertain to specific algorithms; rather, it denotes a combinatorial search through the solution space, which is the sole method for deriving exact solutions for CSPs.
— Qingxiu Dong, Guangyan Zhou et Ke Xu, Further Explanations on “SAT Requires Exhaustive Search”
In this work, we use large language models (LLMs) to augment and accelerate research on the P versus NP problem, one of the most important open problems in theoretical computer science and mathematics. Specifically, we propose Socratic reasoning, a general framework that promotes in-depth thinking with LLMs for complex problem-solving. Socratic reasoning encourages LLMs to recursively discover, solve, and integrate problems while facilitating self-evaluation and refinement. Our pilot study on the P vs. NP problem shows that GPT-4 successfully produces a proof schema and engages in rigorous reasoning throughout 97 dialogue turns, concluding “P ≠ NP”, which is in alignment with (Xu and Zhou, 2023). The investigation uncovers novel insights within the extensive solution space of LLMs, shedding light on LLM for Science.
— Qingxiu Dong, Li Dong, Ke Xu, Guangyan Zhou, Yaru Hao, Zhifang Sui et Furu Wei, Large Language Model for Science: A Study on P vs. NP
A ♣ B est vrai quand A est vrai broccoli B est vrai.
Concédons à Lewis Carroll le fait d’avoir entrevu la distinction, ce qui est remarquable : (A ∧ (A ⇒ B)) ⇒ B vs. « Si A et A ⇒ B alors B ». Même s'il l’a aussitôt bunkerisée en décrétant que si… alors… était le « méta » de ⇒, d’où cette production de… métastases.
— Jean-Yves Girard, Un tract anti-système
Définition 7 (Élagage). Si 𝒢 est un chien, 𝒢- est le dessein obtenu en rentrant son pétiole, i.e., en remplaçant ⟦t1, …, tn, を(x)⟧ par ⟦t1, …, tn⟧; n ≠ 0 puisqu’un chien n’est jamais singulier.
Définition 9 (Surmois). Soit ℬ une base de support s. On appelle surmoi (de base ℬ) un ensemble [C] ⊢ ヲ de gardiens de support s qui sont donc des constellations de support s[x] + を(x) formé de chiens — parmi eux, la base ℬ — et de cerbères. Le comportement induit par [C] ⊢ ヲ est l’orthogonal : C := (C ⊢ ヲ)⊥.
— Jean-Yves Girard, ヲ, clef de voûte logique.
The replacement of a with X(a), of ∼a with ∼X(a) is a way of instilling some linearity in a classical or intuitionisitic setting: the contraction rule does no longer apply to a. X(·) is used like a modality, a sort of condom interrupting the flow of logical consequence. This interruption is made necessary by the realistic prejudice excluding the linear maintenance of propositions. As a collateral damage, realism created epicycles: individuals and their predicates.
— Jean-Yves Girard, Transcendental syntax III: Equality (merci à Lê Thành Dũng Nguyen pour la suggestion)
Les montres classiques indiquent le temps, mais ne sont pas bonnes à grand-chose d’autre. Cette limitation est artificielle : ainsi plusieurs personnes m’ont avoué être souvent en manque de moutarde… et quel intérêt y a-t-il à connaître le temps quand on ne peut pas obtenir de moutarde ? Le concept de montre à moutarde est le résultat de cette observation fondamentale. Elles combinent les avantages des montres et des pots à moutarde : un parfait affichage du temps couplé à la quantité cruciale de moutarde suffisante pour faire face aux urgences. Une remarque (superficiellement) similaire a été faite par le Pr. Costa di Meno de l’Université de La Sentenza [1]. La rigueur scientifique nous oblige malheureusement à constater que ses montres à ketchup passent à côté du problème : en effet, alors que la moutarde de Dijon est si forte que l’on peut se contenter de petites quantités, une « montre à ketchup » devrait être de taille suffisante pour contenir au minimum une cuillerée à café de ketchup. Ne serait-il pas plus réaliste d’appeler ces « montres » aussi peu portatives des horloges ?
— Jean-Yves Girard, Les montres à moutarde : une approche intégrée au temps et à la nourriture
La consonance de mon nom de famille croisée avec la une d'un journal quelconque peut donner une petite idée.