Jean Abou Samra
@jeanas.bsky.social
PhD student in theoretical computer science at Eötvös Loránd University in Budapest. Mainly here to chat about TCS/math.
La presse en parle : www.lemonde.fr/pixels/artic...
L’enquête sur la plateforme X étendue à des « propos négationnistes » publiés par son IA, Grok
Dans la publication visée, qui fait aussi l’objet de plaintes de la Ligue des droits de l’homme et de SOS Racisme, Grok affirme notamment que les chambres à gaz du camp d’extermination nazi d’Auschwit...
www.lemonde.fr
November 19, 2025 at 6:58 PM
La presse en parle : www.lemonde.fr/pixels/artic...
et normal est dénombrablement paracompact, avant d'enchaîner sur le fait que tout de même, il y a quelques implications de base que tout mathématicien devrait connaître, comme le fait que tout espace T₁ pseudonormal est régulier (quelque chose de ce genre).
November 16, 2025 at 1:00 PM
et normal est dénombrablement paracompact, avant d'enchaîner sur le fait que tout de même, il y a quelques implications de base que tout mathématicien devrait connaître, comme le fait que tout espace T₁ pseudonormal est régulier (quelque chose de ce genre).
J'ai récemment ouvert un bouquin de topologie, que je ne retrouve malheureusement pas, dans la préface duquel l'auteur se plaignait que la « botanique » des espaces topologiques était souvent portée à l'excès et qu'on se fichait vraiment de savoir si tout espace dénombrablement métacompact …
November 16, 2025 at 1:00 PM
J'ai récemment ouvert un bouquin de topologie, que je ne retrouve malheureusement pas, dans la préface duquel l'auteur se plaignait que la « botanique » des espaces topologiques était souvent portée à l'excès et qu'on se fichait vraiment de savoir si tout espace dénombrablement métacompact …
Oui, ça s'appelle les maths synthétiques, et c'est un sujet de recherche actif et très intéressant. Et toute personne qui a fait des maths dans le supérieur a très probablement déjà rencontré ce type d'approche : qui a commencé l'analyse avec une construction des nombres réels ?
November 16, 2025 at 11:11 AM
Oui, ça s'appelle les maths synthétiques, et c'est un sujet de recherche actif et très intéressant. Et toute personne qui a fait des maths dans le supérieur a très probablement déjà rencontré ce type d'approche : qui a commencé l'analyse avec une construction des nombres réels ?
C'est quoi, par curiosité ?
November 14, 2025 at 4:12 PM
C'est quoi, par curiosité ?
I actually spent most of the time doing an informal introduction to realizability since the audience was not familiar with it. In case this interests anyone, the slides are here:
jean.abou-samra.fr/talks/2025-1...
jean.abou-samra.fr/talks/2025-1...
jean.abou-samra.fr
November 10, 2025 at 10:32 PM
I actually spent most of the time doing an informal introduction to realizability since the audience was not familiar with it. In case this interests anyone, the slides are here:
jean.abou-samra.fr/talks/2025-1...
jean.abou-samra.fr/talks/2025-1...
C'est sans doute un peu extrême mais personnellement, depuis quelques versions de Fedora (qui arrivent tous les 6 mois), je réinstalle complètement plutôt que de mettre à jour. L'intérêt est surtout de vérifier que les sauvegardes que j'ai suffisent à tout remettre en ordre en cas de pépin.
November 9, 2025 at 2:59 PM
C'est sans doute un peu extrême mais personnellement, depuis quelques versions de Fedora (qui arrivent tous les 6 mois), je réinstalle complètement plutôt que de mettre à jour. L'intérêt est surtout de vérifier que les sauvegardes que j'ai suffisent à tout remettre en ordre en cas de pépin.
La différence étant tout de même que la mise à jour n'augmente pas les exigences matérielles d'une manière qui empêche de l'installer sur une fraction significative du parc existant.
November 9, 2025 at 2:54 PM
La différence étant tout de même que la mise à jour n'augmente pas les exigences matérielles d'une manière qui empêche de l'installer sur une fraction significative du parc existant.
Interesting but can you reduce the internal logic of the sheaf topos to that of the base topos or do you still need to translate the definition of sheaves externally first to define validity in the sheaf topos?
November 9, 2025 at 1:23 PM
Interesting but can you reduce the internal logic of the sheaf topos to that of the base topos or do you still need to translate the definition of sheaves externally first to define validity in the sheaf topos?
Conversely, assume ¬¬q ⇒ q and let r : Ω be such that (r ∨ ¬r) ⇒ q. We want to prove q. It suffices to prove ¬¬q. So assume ¬q and let's prove ⊥. We have ¬¬(r ∨ ¬r) tautologically. Applying it, we are reduced to proving ¬(r ∨ ¬r). So assume r ∨ ¬r. Then q by our initial assumption, contradicting ¬q.
November 8, 2025 at 1:30 AM
Conversely, assume ¬¬q ⇒ q and let r : Ω be such that (r ∨ ¬r) ⇒ q. We want to prove q. It suffices to prove ¬¬q. So assume ¬q and let's prove ⊥. We have ¬¬(r ∨ ¬r) tautologically. Applying it, we are reduced to proving ¬(r ∨ ¬r). So assume r ∨ ¬r. Then q by our initial assumption, contradicting ¬q.
How to prove it:
If ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q, applying this to q gives ((q ∨ ¬q) ⇒ q) ⇒ q, which is equivalent to (¬q ⇒ q) ⇒ q, and in turn to ¬¬q ⇒ q.
If ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q, applying this to q gives ((q ∨ ¬q) ⇒ q) ⇒ q, which is equivalent to (¬q ⇒ q) ⇒ q, and in turn to ¬¬q ⇒ q.
November 8, 2025 at 1:30 AM
How to prove it:
If ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q, applying this to q gives ((q ∨ ¬q) ⇒ q) ⇒ q, which is equivalent to (¬q ⇒ q) ⇒ q, and in turn to ¬¬q ⇒ q.
If ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q, applying this to q gives ((q ∨ ¬q) ⇒ q) ⇒ q, which is equivalent to (¬q ⇒ q) ⇒ q, and in turn to ¬¬q ⇒ q.
The following lemma explains it somewhat:
A truth value q : Ω is classical (i.e., ¬¬q ⇒ q) iff ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q.
A truth value q : Ω is classical (i.e., ¬¬q ⇒ q) iff ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q.
November 8, 2025 at 12:46 AM
The following lemma explains it somewhat:
A truth value q : Ω is classical (i.e., ¬¬q ⇒ q) iff ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q.
A truth value q : Ω is classical (i.e., ¬¬q ⇒ q) iff ∀ r : Ω, ((r ∨ ¬r) ⇒ q) ⇒ q.
I'm putting that one on my students' exercise sheets 🙂
November 8, 2025 at 12:22 AM
I'm putting that one on my students' exercise sheets 🙂
Tu sais, moi, après bsky.app/profile/jean..., je ne m'étonne plus de rien.
This crank paper that I was linking for fun last year has been published in a Springer journal 😱
blog.computationalcomplexity.org/2025/08/some...
blog.computationalcomplexity.org/2025/08/some...
November 7, 2025 at 9:46 PM
Tu sais, moi, après bsky.app/profile/jean..., je ne m'étonne plus de rien.
On ne l'apprend jamais. (Pour la petite histoire, quand mes parents m'ont appris à compter les dizaines plus tôt qu'à l'école, ils ont utilisé la manière belge/suisse pour faire plus simple, ce qui paraît-il a amusé quelques institutrices.)
November 7, 2025 at 5:11 PM
On ne l'apprend jamais. (Pour la petite histoire, quand mes parents m'ont appris à compter les dizaines plus tôt qu'à l'école, ils ont utilisé la manière belge/suisse pour faire plus simple, ce qui paraît-il a amusé quelques institutrices.)
Mais moi non plus, je ne suis pas très au point sur ces trucs. Et je n'ai pas compris la dernière question.
November 7, 2025 at 9:57 AM
Mais moi non plus, je ne suis pas très au point sur ces trucs. Et je n'ai pas compris la dernière question.
Je crois que l'arithmétique des types finis intuitionniste est strictement intermédiaire (en termes de force de cohérence, de fonctions définissables, etc.) entre l'arithmétique du premier ordre intuitionniste et l'arithmétique d'ordre supérieur intuitionniste.
November 7, 2025 at 9:57 AM
Je crois que l'arithmétique des types finis intuitionniste est strictement intermédiaire (en termes de force de cohérence, de fonctions définissables, etc.) entre l'arithmétique du premier ordre intuitionniste et l'arithmétique d'ordre supérieur intuitionniste.
Je peux prouver que tout ensemble définissable dans FO(ℝ; +, -, 0) est une combinaison booléenne de sous-espaces vectoriels et en déduire que ℝ⁺ n'est pas définissable.
Pour FO(ℝ; +, -, 0, 1), je n'ai pas vérifié mais je pense que la même histoire doit se répéter avec des sous-espaces affines.
Pour FO(ℝ; +, -, 0, 1), je n'ai pas vérifié mais je pense que la même histoire doit se répéter avec des sous-espaces affines.
November 5, 2025 at 8:14 PM
Je peux prouver que tout ensemble définissable dans FO(ℝ; +, -, 0) est une combinaison booléenne de sous-espaces vectoriels et en déduire que ℝ⁺ n'est pas définissable.
Pour FO(ℝ; +, -, 0, 1), je n'ai pas vérifié mais je pense que la même histoire doit se répéter avec des sous-espaces affines.
Pour FO(ℝ; +, -, 0, 1), je n'ai pas vérifié mais je pense que la même histoire doit se répéter avec des sous-espaces affines.
Sorry, I don't know what a 2-random sequence is and I don't have the time to learn it right now.
November 5, 2025 at 8:27 AM
Sorry, I don't know what a 2-random sequence is and I don't have the time to learn it right now.
Yes, we just need to reason about codings of proofs, so PA or even much weaker things suffice.
November 3, 2025 at 10:05 PM
Yes, we just need to reason about codings of proofs, so PA or even much weaker things suffice.
Beware not to confuse this with the following statement: ZFC proves that there is an algorithm which, if run with the input BB(644), outputs the consistency of ZFC as a boolean. That one is also correct, but trivial — a constant program will do.
November 3, 2025 at 9:41 PM
Beware not to confuse this with the following statement: ZFC proves that there is an algorithm which, if run with the input BB(644), outputs the consistency of ZFC as a boolean. That one is also correct, but trivial — a constant program will do.
If you interpret the informal "know"s in a certain particular way, yes. A precise and correct statement is that there exists an algorithm such that ZFC proves that the algorithm run with input BB(643) outputs the consistency of ZFC as a boolean.
November 3, 2025 at 9:41 PM
If you interpret the informal "know"s in a certain particular way, yes. A precise and correct statement is that there exists an algorithm such that ZFC proves that the algorithm run with input BB(643) outputs the consistency of ZFC as a boolean.