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.
Is Agda a homage to Henk Barendregt?
September 5, 2025 at 1:44 PM
Is Agda a homage to Henk Barendregt?
Dear combinatorialists of Bluesky (@pyviv.bsky.social?),
I had to sweat quite a bit to find the following formula for expressing x^m⋅binom(x, n) as a linear combination with coefficients polynomial in n of binom(x, n), …, binom(x, n+m). Does it ring a bell?
I had to sweat quite a bit to find the following formula for expressing x^m⋅binom(x, n) as a linear combination with coefficients polynomial in n of binom(x, n), …, binom(x, n+m). Does it ring a bell?
June 23, 2025 at 9:05 AM
Dear combinatorialists of Bluesky (@pyviv.bsky.social?),
I had to sweat quite a bit to find the following formula for expressing x^m⋅binom(x, n) as a linear combination with coefficients polynomial in n of binom(x, n), …, binom(x, n+m). Does it ring a bell?
I had to sweat quite a bit to find the following formula for expressing x^m⋅binom(x, n) as a linear combination with coefficients polynomial in n of binom(x, n), …, binom(x, n+m). Does it ring a bell?
Before I edit this, can anyone actually competent in algebra confirm that I'm not going mad in thinking that Wikipedia's formula for ℚ(α) on en.wikipedia.org/wiki/Algebra... is completely wrong?
June 5, 2025 at 2:36 PM
Before I edit this, can anyone actually competent in algebra confirm that I'm not going mad in thinking that Wikipedia's formula for ℚ(α) on en.wikipedia.org/wiki/Algebra... is completely wrong?
I am presently working with matrices with coefficients in matrices with coefficients in polynomials with coefficients in p-adic integers.
My 2-adic sheep dreams look more like:
My 2-adic sheep dreams look more like:
May 27, 2025 at 10:00 AM
I am presently working with matrices with coefficients in matrices with coefficients in polynomials with coefficients in p-adic integers.
My 2-adic sheep dreams look more like:
My 2-adic sheep dreams look more like:
From the same paper arxiv.org/pdf/2505.00682 :
May 15, 2025 at 4:53 PM
From the same paper arxiv.org/pdf/2505.00682 :
This is, apparently, an actual commutative diagram excerpted from an actual math paper. (Seen on mathstodon.xyz/@highergeome...)
May 15, 2025 at 4:52 PM
This is, apparently, an actual commutative diagram excerpted from an actual math paper. (Seen on mathstodon.xyz/@highergeome...)
More precisely: the core of the reduction is this typing environment. The type to inhabit is ▲. The argument is that an inhabitant must be successively applying all these hypotheses, forming a solution to a diophantine equation. But in realizability, we have to make sure
May 15, 2025 at 10:24 AM
More precisely: the core of the reduction is this typing environment. The type to inhabit is ▲. The argument is that an inhabitant must be successively applying all these hypotheses, forming a solution to a diophantine equation. But in realizability, we have to make sure
Mon navigateur est en français. Je vois bien "Accept-Language: fr" dans les requêtes, et le reste de Trainline s'affiche en français.
Exemple :
Exemple :
April 25, 2025 at 2:55 PM
Mon navigateur est en français. Je vois bien "Accept-Language: fr" dans les requêtes, et le reste de Trainline s'affiche en français.
Exemple :
Exemple :
In what sense do you mean that the pullback of the image “is” the image of the pullback: do you just require a blue iso such that the red triangle commutes or do you also require it to make the green pentagon commute?
April 22, 2025 at 5:07 PM
In what sense do you mean that the pullback of the image “is” the image of the pullback: do you just require a blue iso such that the red triangle commutes or do you also require it to make the green pentagon commute?
… must be a Heyting prealgebra, and the operations ⊤, ⊥, ∧, ∨, ⇒ quotient to the usual Heyting algebra operations in the Heyting algebra reflection.
Now fold the weakening rule into the axiom rule as in the second picture. To my surprise when I wrote this down, I do not see how to recover the fact.
Now fold the weakening rule into the axiom rule as in the second picture. To my surprise when I wrote this down, I do not see how to recover the fact.
April 14, 2025 at 4:08 PM
… must be a Heyting prealgebra, and the operations ⊤, ⊥, ∧, ∨, ⇒ quotient to the usual Heyting algebra operations in the Heyting algebra reflection.
Now fold the weakening rule into the axiom rule as in the second picture. To my surprise when I wrote this down, I do not see how to recover the fact.
Now fold the weakening rule into the axiom rule as in the second picture. To my surprise when I wrote this down, I do not see how to recover the fact.
Here is a natural deduction system for intuitionistic propositional logic. If X is a set endowed with elements ⊤, ⊥ of X, binary operations ∧, ∨, ⇒ on X and a relation ⊢ between finite subsets of X and elements of X, then it is straightforward if tedious to show that (X ≤) where a ≤ b :⇔ {a} ≤ b …
April 14, 2025 at 4:08 PM
Here is a natural deduction system for intuitionistic propositional logic. If X is a set endowed with elements ⊤, ⊥ of X, binary operations ∧, ∨, ⇒ on X and a relation ⊢ between finite subsets of X and elements of X, then it is straightforward if tedious to show that (X ≤) where a ≤ b :⇔ {a} ≤ b …
This comic is spot on: www.smbc-comics.com/comic/what-i...
April 9, 2025 at 3:01 PM
This comic is spot on: www.smbc-comics.com/comic/what-i...
@wildverzweigt.bsky.social So apparently you're a set! I thought you were a true truth value, but AIs know this better of course.
(Shared by John Carlos Baez on Mastodon mathstodon.xyz/@johncarlosb...)
(Shared by John Carlos Baez on Mastodon mathstodon.xyz/@johncarlosb...)
March 10, 2025 at 9:03 PM
@wildverzweigt.bsky.social So apparently you're a set! I thought you were a true truth value, but AIs know this better of course.
(Shared by John Carlos Baez on Mastodon mathstodon.xyz/@johncarlosb...)
(Shared by John Carlos Baez on Mastodon mathstodon.xyz/@johncarlosb...)
Je l'ai fait et j'invite chacun à faire de même.
March 3, 2025 at 10:53 PM
Je l'ai fait et j'invite chacun à faire de même.
February 16, 2025 at 1:06 AM
That's a good question! I'm not sure who first used the term “canonicity”, but I found the concept as early as in Per Martin-Löf's original paper on MLTT from 1972 (discarding his preprint from the previous year with the theory shown inconsistent by Girard). raw.githubusercontent.com/michaelt/mar...
February 8, 2025 at 11:44 AM
That's a good question! I'm not sure who first used the term “canonicity”, but I found the concept as early as in Per Martin-Löf's original paper on MLTT from 1972 (discarding his preprint from the previous year with the theory shown inconsistent by Girard). raw.githubusercontent.com/michaelt/mar...
“Free, uncensored speech”
January 13, 2025 at 4:28 PM
“Free, uncensored speech”
With credits to my supervisor Joël Ouaknine, here is a cute Christmas problem. (It would be embarrassing if I told how much time I took to solve it.)
On a Christmas tree, there are two tinsels which are tied together at the same point at the bottom of the tree, and at another point at the top.
On a Christmas tree, there are two tinsels which are tied together at the same point at the bottom of the tree, and at another point at the top.
January 9, 2025 at 11:39 AM
With credits to my supervisor Joël Ouaknine, here is a cute Christmas problem. (It would be embarrassing if I told how much time I took to solve it.)
On a Christmas tree, there are two tinsels which are tied together at the same point at the bottom of the tree, and at another point at the top.
On a Christmas tree, there are two tinsels which are tied together at the same point at the bottom of the tree, and at another point at the top.
En ce moment, à chaque fois que je me dis que le monde a touché le fond au niveau politique, il parvient à s'enfoncer plus bas.
January 6, 2025 at 9:20 PM
En ce moment, à chaque fois que je me dis que le monde a touché le fond au niveau politique, il parvient à s'enfoncer plus bas.
That's clearly a bug fix: the output of js_get_stack_pointer() is saved by the JavaScript interpreter on initialization, but if quickjs is embedded, then initialization might happen at a low stack frame (on a long call stack), then later uses of the engine could be higher on the stack, …
December 8, 2024 at 11:48 PM
That's clearly a bug fix: the output of js_get_stack_pointer() is saved by the JavaScript interpreter on initialization, but if quickjs is embedded, then initialization might happen at a low stack frame (on a long call stack), then later uses of the engine could be higher on the stack, …
But the material is easy, isn't it?
December 8, 2024 at 12:21 AM
But the material is easy, isn't it?