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.
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.
(The consistency assumption is needed, for otherwise ZFC proves BB(643) = 0, and also BB(643) = 54230 or whatever number, since ZFC proves everything.)
I think “this number is just out of the reach of our knowledge” is a better intuition than “this number has a special power to destroy ZFC”.
I think “this number is just out of the reach of our knowledge” is a better intuition than “this number has a special power to destroy ZFC”.
November 3, 2025 at 9:06 PM
(The consistency assumption is needed, for otherwise ZFC proves BB(643) = 0, and also BB(643) = 54230 or whatever number, since ZFC proves everything.)
I think “this number is just out of the reach of our knowledge” is a better intuition than “this number has a special power to destroy ZFC”.
I think “this number is just out of the reach of our knowledge” is a better intuition than “this number has a special power to destroy ZFC”.
If it sounds impressive, put it in the contrapositive: Assuming ZFC is consistent, there is no n ∈ ℕ such that ZFC can prove that BB(643) = n. Now it sounds less impressive, doesn't it?
November 3, 2025 at 9:06 PM
If it sounds impressive, put it in the contrapositive: Assuming ZFC is consistent, there is no n ∈ ℕ such that ZFC can prove that BB(643) = n. Now it sounds less impressive, doesn't it?
Not that if there is n ∈ ℕ such that BB(643) = n then ZFC is inconsistent (obviously), and also not that if there is n ∈ ℕ such that “I know that BB(643) = n” then ZFC is inconsistent — “I know” doesn't have a well-defined mathematical meaning.
November 3, 2025 at 9:06 PM
Not that if there is n ∈ ℕ such that BB(643) = n then ZFC is inconsistent (obviously), and also not that if there is n ∈ ℕ such that “I know that BB(643) = n” then ZFC is inconsistent — “I know” doesn't have a well-defined mathematical meaning.
Not really… First the argument is different than making Turing machines stop faster, but most importantly, I think you're confusing truth and provability. What is true is that if there exists an n ∈ ℕ such that *ZFC proves that BB(643) = n*, then ZFC is inconsistent.
November 3, 2025 at 9:06 PM
Not really… First the argument is different than making Turing machines stop faster, but most importantly, I think you're confusing truth and provability. What is true is that if there exists an n ∈ ℕ such that *ZFC proves that BB(643) = n*, then ZFC is inconsistent.
“BB(643) makes ZFC inconsistent” What do you mean? Its value is just independent of ZFC, I don't see any inconsistency involved.
November 3, 2025 at 7:04 PM
“BB(643) makes ZFC inconsistent” What do you mean? Its value is just independent of ZFC, I don't see any inconsistency involved.
is to study the construction that turns an elementary 1-topos into a model of type theory, since those are much simpler to deal with.) At least the nice thing with math is that we don't need to read the works of X to understand the ideas of X. Hopefully more expositions of HoTT will follow Egbert's.
October 31, 2025 at 9:30 PM
is to study the construction that turns an elementary 1-topos into a model of type theory, since those are much simpler to deal with.) At least the nice thing with math is that we don't need to read the works of X to understand the ideas of X. Hopefully more expositions of HoTT will follow Egbert's.