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 was asked to give a talk today at our informal type theory seminar in Budapest and chose to present (and hopefully not misrepresent) Andrej Bauer and James E. Hanson's paper on making the reals countable in constructive mathematics.
November 10, 2025 at 10:32 PM
I was asked to give a talk today at our informal type theory seminar in Budapest and chose to present (and hopefully not misrepresent) Andrej Bauer and James E. Hanson's paper on making the reals countable in constructive mathematics.
A paper just dropped on arXiv claims to solve parity games in polynomial time, which if correct is a huge result. This is not my area, but if anyone here looks at it, I'm curious to know how it went.
arxiv.org/abs/2511.03752
arxiv.org/abs/2511.03752
Attractors Is All You Need: Parity Games In Polynomial Time
This paper provides a polynomial-time algorithm for solving parity games that runs in $\mathcal{O}(n^{2}\cdot(n + m))$ time-ending a search that has taken decades. Unlike previous attractor-based algo...
arxiv.org
November 7, 2025 at 10:29 AM
A paper just dropped on arXiv claims to solve parity games in polynomial time, which if correct is a huge result. This is not my area, but if anyone here looks at it, I'm curious to know how it went.
arxiv.org/abs/2511.03752
arxiv.org/abs/2511.03752
I'm happy to hear that Egbert Rijke's book “Introduction to Homotopy Type Theory” is finally published by Cambridge University Press!
www.cambridge.org/us/universit...
www.cambridge.org/us/universit...
Introduction to Homotopy Type Theory | Cambridge University Press & Assessment
www.cambridge.org
October 31, 2025 at 4:55 PM
I'm happy to hear that Egbert Rijke's book “Introduction to Homotopy Type Theory” is finally published by Cambridge University Press!
www.cambridge.org/us/universit...
www.cambridge.org/us/universit...
Where can I find a proof that unique choice is valid in an elementary 1-topos? (I'd like an actual proof, not "it is easy to see that" or "exercise".)
October 30, 2025 at 12:35 PM
Where can I find a proof that unique choice is valid in an elementary 1-topos? (I'd like an actual proof, not "it is easy to see that" or "exercise".)
Reposted by Jean Abou Samra
Reposted by Jean Abou Samra
Now thinking about the following mathematical game:
‣ Three players. “Arthur” and “Nimue” are allied against “Merlin”. Merlin first chooses a bit b∈{0,1} and shows it to Nimue (not Arthur). Arthur's goal is to guess b, and Nimue (knowing b) tries to help him guess. But Nimue can't communicate …
‣ Three players. “Arthur” and “Nimue” are allied against “Merlin”. Merlin first chooses a bit b∈{0,1} and shows it to Nimue (not Arthur). Arthur's goal is to guess b, and Nimue (knowing b) tries to help him guess. But Nimue can't communicate …
October 27, 2025 at 9:53 AM
Now thinking about the following mathematical game:
‣ Three players. “Arthur” and “Nimue” are allied against “Merlin”. Merlin first chooses a bit b∈{0,1} and shows it to Nimue (not Arthur). Arthur's goal is to guess b, and Nimue (knowing b) tries to help him guess. But Nimue can't communicate …
‣ Three players. “Arthur” and “Nimue” are allied against “Merlin”. Merlin first chooses a bit b∈{0,1} and shows it to Nimue (not Arthur). Arthur's goal is to guess b, and Nimue (knowing b) tries to help him guess. But Nimue can't communicate …
Reposted by Jean Abou Samra
"I was never sure if I would succeed in academia, so my plan B was always to become a high school teacher."
—Peter Scholze, Fields Medallist (became the youngest full professor in Germany when he was 24)
—Peter Scholze, Fields Medallist (became the youngest full professor in Germany when he was 24)
October 27, 2025 at 12:14 AM
"I was never sure if I would succeed in academia, so my plan B was always to become a high school teacher."
—Peter Scholze, Fields Medallist (became the youngest full professor in Germany when he was 24)
—Peter Scholze, Fields Medallist (became the youngest full professor in Germany when he was 24)
This week was the 7th Rocq tutorial session in the course I'm TAing, and so far not one student noticed that we're working anti-classically.
October 22, 2025 at 8:28 PM
This week was the 7th Rocq tutorial session in the course I'm TAing, and so far not one student noticed that we're working anti-classically.
Mathematicians: In type theory, objects can be equal in more than one way? Are you insane?!?!
Me: Wait until you've seen the model where there are infinitely many endofunctions on a singleton…
Me: Wait until you've seen the model where there are infinitely many endofunctions on a singleton…
October 20, 2025 at 7:27 PM
Mathematicians: In type theory, objects can be equal in more than one way? Are you insane?!?!
Me: Wait until you've seen the model where there are infinitely many endofunctions on a singleton…
Me: Wait until you've seen the model where there are infinitely many endofunctions on a singleton…
@gro-tsen.bsky.social math.stackexchange.com/questions/51...
(from @ncfavier.bsky.social on the Fediverse)
(from @ncfavier.bsky.social on the Fediverse)
Does "$\mathbb R$ is the disjoint union of two non-empty sets" imply $\mathbb R = (-\infty,0] \cup (0,+\infty)$?
Consider IZF (Intuitionistic Zermelo-Fraenkel set theory) with the added axiom that there exist two non-emtpy subsets $A, B$ of $\mathbb R$ such that $\mathbb R$ is the disjoint union of $A$ and $B$.
math.stackexchange.com
October 18, 2025 at 4:29 PM
@gro-tsen.bsky.social math.stackexchange.com/questions/51...
(from @ncfavier.bsky.social on the Fediverse)
(from @ncfavier.bsky.social on the Fediverse)
Microsoft introduces AI facial recognition to OneDrive photos and the preferences say: “You can only turn off this setting 3 times a year.”
This is enshittification taken to the next level.
hardware.slashdot.org/story/25/10/...
This is enshittification taken to the next level.
hardware.slashdot.org/story/25/10/...
Microsoft's OneDrive Begins Testing Face-Recognizing AI for Photos (for Some Preview Users) - Slashdot
I uploaded a photo on my phone to Microsoft's "OneDrive" file-hosting app — and there was a surprise waiting under Privacy and Permissions. "OneDrive uses AI to recognize faces in your photos.....
hardware.slashdot.org
October 16, 2025 at 5:59 PM
Microsoft introduces AI facial recognition to OneDrive photos and the preferences say: “You can only turn off this setting 3 times a year.”
This is enshittification taken to the next level.
hardware.slashdot.org/story/25/10/...
This is enshittification taken to the next level.
hardware.slashdot.org/story/25/10/...
“After age 40 I also started to lose the ability I always took for granted: to get to the board at any time and start lecturing on some subject in my field with full proofs without any preparation. …
October 15, 2025 at 6:46 PM
“After age 40 I also started to lose the ability I always took for granted: to get to the board at any time and start lecturing on some subject in my field with full proofs without any preparation. …
Doofus algebra question here. Is there any sort of classification of finitely generated modules over ℤ[X]? If this is intractable, what about submodules of ℤ[X]^d? The usual structure theorem applies to a PID, which ℤ[X] is not.
October 13, 2025 at 10:47 PM
Doofus algebra question here. Is there any sort of classification of finitely generated modules over ℤ[X]? If this is intractable, what about submodules of ℤ[X]^d? The usual structure theorem applies to a PID, which ℤ[X] is not.
I've just finished a complete overhaul of the Wikipedia page on filters:
en.wikipedia.org/wiki/Filter_...
(compare with the previous version: en.wikipedia.org/w/index.php?...)
en.wikipedia.org/wiki/Filter_...
(compare with the previous version: en.wikipedia.org/w/index.php?...)
Filter on a set - Wikipedia
en.wikipedia.org
October 12, 2025 at 10:02 PM
I've just finished a complete overhaul of the Wikipedia page on filters:
en.wikipedia.org/wiki/Filter_...
(compare with the previous version: en.wikipedia.org/w/index.php?...)
en.wikipedia.org/wiki/Filter_...
(compare with the previous version: en.wikipedia.org/w/index.php?...)
Finally! Wikipedia on mobile will no longer redirect to a "m" subdomain, and instead just serve the mobile version on the main domain. No more confusion when you open a link on desktop that was sent by someone on mobile.
www.mediawiki.org/wiki/Request...
www.mediawiki.org/wiki/Request...
Requests for comment/Mobile domain sunsetting/2025 Announcement - MediaWiki
www.mediawiki.org
October 9, 2025 at 12:03 PM
Finally! Wikipedia on mobile will no longer redirect to a "m" subdomain, and instead just serve the mobile version on the main domain. No more confusion when you open a link on desktop that was sent by someone on mobile.
www.mediawiki.org/wiki/Request...
www.mediawiki.org/wiki/Request...
I hate the concept from GitHub, copied by GitLab, Forgejo, Pagure and now Tangled, that you can't contribute to a project without an entire “fork” under your user namespace with its own project page, issues, pull requests, wiki and whatnot, and takes getting past many warnings to delete, etc.
October 5, 2025 at 11:11 PM
I hate the concept from GitHub, copied by GitLab, Forgejo, Pagure and now Tangled, that you can't contribute to a project without an entire “fork” under your user namespace with its own project page, issues, pull requests, wiki and whatnot, and takes getting past many warnings to delete, etc.
I wrote a MathOverflow answer to explain my intuition of the Yoneda lemma, maybe it's useful to someone:
mathoverflow.net/a/501166/519...
mathoverflow.net/a/501166/519...
"Philosophical" meaning of the Yoneda Lemma
The Yoneda Lemma is a simple result of category theory, and its proof is very straightforward.
Yet I feel like I do not truly understand what it is about; I have seen a few comments here mentionin...
mathoverflow.net
October 3, 2025 at 11:57 PM
I wrote a MathOverflow answer to explain my intuition of the Yoneda lemma, maybe it's useful to someone:
mathoverflow.net/a/501166/519...
mathoverflow.net/a/501166/519...
In case anyone is wondering why my Mastodon server is down: in a masterful demonstration of doofosity, I have managed to delete at the same time the Mastodon database and the backup of that database I had just made…
I think I'll go back to my previous account mathstodon.xyz/@jeanas
I think I'll go back to my previous account mathstodon.xyz/@jeanas
Jean Abou Samra (@[email protected])
149 Posts, 5 Following, 1 Follower ·
mathstodon.xyz
September 28, 2025 at 10:37 AM
In case anyone is wondering why my Mastodon server is down: in a masterful demonstration of doofosity, I have managed to delete at the same time the Mastodon database and the backup of that database I had just made…
I think I'll go back to my previous account mathstodon.xyz/@jeanas
I think I'll go back to my previous account mathstodon.xyz/@jeanas
This was an enjoyable talk by Jon Sterling yesterday. I hope his project of building a new proof assistant for HoTT takes off.
www.youtube.com/watch?v=7oBk...
www.youtube.com/watch?v=7oBk...
Jon Sterling, Is it time for a new proof assistant?
YouTube video by HoTTEST
www.youtube.com
September 26, 2025 at 8:02 AM
This was an enjoyable talk by Jon Sterling yesterday. I hope his project of building a new proof assistant for HoTT takes off.
www.youtube.com/watch?v=7oBk...
www.youtube.com/watch?v=7oBk...
Reposted by Jean Abou Samra
I asked a question on MathOverflow about a variation on Medvedev reducibility (definitions are given in the question) which seems interesting to me and I'd like to know if it has been considered before: mathoverflow.net/q/500856/17064
Have you seen this variation of Medvedev reducibility?
In what follows, $A, B$ will denote subsets of $\mathbb{N}^{\mathbb{N}}$, i.e., sets of total functions $\mathbb{N} \to \mathbb{N}$ (maybe assume them to be inhabited to avoid any headaches about the
mathoverflow.net
September 25, 2025 at 8:35 PM
I asked a question on MathOverflow about a variation on Medvedev reducibility (definitions are given in the question) which seems interesting to me and I'd like to know if it has been considered before: mathoverflow.net/q/500856/17064
Reposted by Jean Abou Samra
Vous pouvez soutenir ma proposition à la Cour des Comptes d'examiner les marchés publics de voyagistes, notamment dans l'ESR :
participationcitoyenne.ccomptes.fr/processes/co...
participationcitoyenne.ccomptes.fr/processes/co...
Les marchés publics de voyagistes - Contributions - 2025 - Aidez-nous à enrichir notre programme de travail - Plateforme de participation de la Cour des Comptes
Corps de la contributionLes administrations et opérateurs publics, notamment ceux de l'enseignement supérieur et de la recherche, fond appel à des agences de voyage (FCM, TravelPlanet…) pour l'hôtelle...
participationcitoyenne.ccomptes.fr
September 25, 2025 at 10:28 AM
Vous pouvez soutenir ma proposition à la Cour des Comptes d'examiner les marchés publics de voyagistes, notamment dans l'ESR :
participationcitoyenne.ccomptes.fr/processes/co...
participationcitoyenne.ccomptes.fr/processes/co...
This is a great read on the attacks on Wikipedia over alledged bias:
www.theverge.com/cs/features/...
www.theverge.com/cs/features/...
Wikipedia is under attack — and how it can survive
The site’s volunteers face threats from Trump, billionaires, and AI.
www.theverge.com
September 16, 2025 at 12:37 AM
This is a great read on the attacks on Wikipedia over alledged bias:
www.theverge.com/cs/features/...
www.theverge.com/cs/features/...
You know you're in the right place to discuss HoTT when you hear that ℤ is inductively generated by a point in ℤ and an equality ℤ = ℤ.
September 9, 2025 at 4:03 PM
You know you're in the right place to discuss HoTT when you hear that ℤ is inductively generated by a point in ℤ and an equality ℤ = ℤ.