Jean Abou Samra (new account)

PhD student in theoretical computer science at Eötvös Loránd University in Budapest. Mainly here to chat about TCS/math.

Public Key

npub14pv6xjcsz2qa6tctew034s5wsj5p2xuh65q86qe6gpegaslstc6qjhtzwd

NIP-05 Address

jeanas@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqs2skdrfvgp9qwa9u9uh8c6c28gf2q4rwta2qraqvayqu5wc0c9udqpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0ds6scsq3

Publishing to

relay.damus.io

nos.lol

Author Public Key

npub14pv6xjcsz2qa6tctew034s5wsj5p2xuh65q86qe6gpegaslstc6qjhtzwd

Show more details

Last Notes

2026-03-27 19:22:02 UTC

I just signed the “No free view? No review!" pledge to refuse reviewing papers for closed-access venues, and I encourage all researchers to do the same.
https://nofreeviewnoreview.org

2026-02-09 18:41:02 UTC

- reply

@nprofile…d423 I just heard this as an actual, unintentional lapsus 😄

2026-02-09 12:25:22 UTC

nLab doesn't require CwFs to have a terminal object. Is there any use for this generality?

2026-02-08 21:33:35 UTC

- reply

@nprofile…l3hr FYI a definitional isomorphism is an isomorphism where the roundtrips hold definitionally (i.e., f : A → B and g : B → A with x : A ⊢ g(f(x)) = x and y : B ⊢ f(g(y)) = y).

2026-02-07 13:55:09 UTC

- reply

@nprofile…ktlj I mean, the failure of one specific attempt at making definitional equality stronger in a specific way doesn't imply the general idea is necessarily stupid or doomed.

2026-02-07 01:08:52 UTC

- reply

@nprofile…d423 Well, we aren't sure yet what HOTT should be precisely. Ask again in a year.

2026-02-07 00:45:22 UTC

- reply

@nprofile…d423 And in HOTT we would ideally like to get both. But we are not sure yet if it's possible.

2026-01-29 21:11:49 UTC

- reply

@nprofile…k4ws Does this help? https://proofassistants.stackexchange.com/a/5267/

2026-01-25 20:06:35 UTC

- reply

@nprofile…47dl There's @jpoiret.

2026-01-09 15:36:30 UTC

- reply

@nprofile…lfhd Have you seen all the recent discussions here about the enshittification of ACM? e.g., https://mathstodon.xyz/@jonmsterling/115820871542282502
Facebook also explicitly allows LGBT+phobia specifically in its usage conditions. https://www.assomousse.org/plainte-contre-meta-et-mark-zuckerberg-pour-injures-et-discriminations-lgbtphobes/

2026-01-07 21:48:59 UTC

- reply

Finally! I've answered the question.

2026-01-07 17:55:05 UTC

- reply

@nprofile…ktlj By the way, is there a way to solve this case without changing the definition of _divides?_wf_ ?

2026-01-07 17:48:08 UTC

- reply

@nprofile…ktlj Great project! My pet peeve is the error message for ill-typed with-abstractions. It tells me that the type of some internally generated function is ill-typed and displays that big type. I'd really like it to pinpoint to a specific subterm that's ill-typed (as if I had written that function myself). Here's a toy example from some code I happened to be working on: https://gitlab.com/-/snippets/4922467

2026-01-07 17:17:47 UTC

- reply

@nprofile…ge3w Maybe ask the Lean people on https://leanprover.zulipchat.com . I've seen a lot of talk about AI tools for formalization there lately.

2026-01-05 08:35:35 UTC

- reply

@nprofile…xuzd I am surprised to hear that a serious researcher with credentials like you is having trouble getting a paper past arXiv moderation, given the amount of blatant LLM slop I've seen there lately, most of it from people outside academia. What are they complaining about?

2026-01-02 22:07:05 UTC

@nprofile…xeuj @nprofile…gy4l @nprofile…xuzd @nprofile…52gx If you need to convince anyone, tell them to look at Wikipedia. It has browser-local user preferences, account log-in, etc., and no cookie banner whatsoever. What matters is not whether you store any cookies but whether the user consented to your using their data in the way you do.

2025-12-29 20:12:31 UTC

- reply

Solved (positively), at last. Now I need to figure out what this implies for the original problem.

2025-12-27 16:20:03 UTC

- reply

@nprofile…w8t5 @nprofile…356e The Dedukti project is devoted to interoperability between proof assistants. I must unfortunately say I am skeptical of the approach but at least it's a try and they do manage to achieve some amount of interoperability.

2025-12-25 13:02:57 UTC

- reply

Looking at it with a fresh eye, I realized that the question is actually quite easy. Now let me see what this implies for the original problem.

2025-12-25 09:38:26 UTC

- reply

@nprofile…ztfm I see. I'd gladly fire up wget and try to help more, but I'm on very limited Internet access for a week.

2025-12-25 08:09:04 UTC

- reply

@nprofile…fdxu @nprofile…ztfm Try this snapshot taken by Internet Archive today: https://web.archive.org/web/20251225074846/https://set.adelaide.edu.au/geometry-applications/
This is the page where you can trigger a crawl: https://web.archive.org/save

2025-12-18 23:17:27 UTC

- reply

@nprofile…dh59 Coquand paradox of trees might come closer (?) but it uses W-types.

2025-12-18 23:16:10 UTC

- reply

@nprofile…dh59 Well, I haven't seen *any* version of Russell's paradox in type theory in the first place. Have you? Or is that actually your question (I understood it was about restricting the type theory in which a paradox occurs)?

2025-12-18 23:13:38 UTC

- reply

@nprofile…dh59 Doesn't Girard's paradox work? He formulated it as the inconsistency of a certain pure type system, and these have just universes and Pi types.

2025-12-14 16:59:16 UTC

- reply

@nprofile…rrqe I'm glad you're implementing your proof assistant with this in mind. Lean is excellent in many respects but (although everybody talks about this as an advantage over other proof assistants) I never got used to its editing experience. I find it super distracting to have the infoview updating constantly with new errors and warnings as I type. Not to mention the frustration when I stare at the goal thinking, start writing a tactic, and the error on the incomplete line makes the goal disappear.

2025-12-09 06:39:26 UTC

- reply

@nprofile…ztfm My thought is that moving has a pretty high cost, but the possibility of it can and should in the short term be used as a negotiation lever with StackExchange to keep them honest about respecting the agreement.

2025-12-08 19:11:10 UTC

- reply

@nprofile…v38n Great! Can we see the result?

2025-12-06 23:26:34 UTC

I thought a bit about the question https://mathoverflow.net/q/503195/ and arrived at the following little problem of computability. Any ideas? It happens to involve something like the “parameterized realizability” from @nprofile…99up's and @nprofile…kgh3's paper https://arxiv.org/abs/2404.01256.
Let A, B ⊆ ℕ be disjoint. Assume that there is a program M which, given x ∈ A ∪ B, decides whether x ∈ A or x ∈ B, but with some help. Namely, there is a “desired oracle” which is an infinite word on four letters, and M has access to a “noisy” version of this oracle, which can be anything satisfying a requirement (that's the “parameterized” part: M must work given any oracle from a certain set; but unlike the countable reals paper, here the set will also depend on the input x). The requirement is the following: Arrange the four letters into a 2×2 table. Then if x ∈ A, the n-th letters of the desired and actual oracle must be on the same line of the table, while if x ∈ B they must be on the same column.
The question is: Must there be another program M' which does the same but without the help?
The difficulty is this: If M “knows” the n-th letter of the desired oracle (it manages to compute it somehow), and the n-th letter of the actual oracle is different, then M can deduce whether x ∈ A or x ∈ B. But if the actual oracle is the same as the desired one, then M can use that as computational power.
If I try to create M', I'd like to make it run M on well-chosen actual oracles. Those letters of the desired oracle which M “knows” should match in the actual oracle. But M' can't make everything match because it also has to work computably. So how to extract what exactly M knows in order to replicate it?

2025-12-03 21:27:16 UTC

- reply

@nprofile…yqfl Yeah I knew this under the name “type of partial elements”.

2025-12-03 21:18:02 UTC

- reply

@nprofile…yqfl Oh you mean the partiality monad?

2025-12-03 21:08:40 UTC

- reply

@nprofile…yqfl What is the Rosolini lifting monad?

2025-12-03 10:42:38 UTC

- reply

@nprofile…9fhr Wait, doesn't Lean also fit your criteria?

2025-12-02 01:04:26 UTC

- reply

@nprofile…dh59 The way I learnt it, you don't put any eta at all in the reduction relation (or at most function eta). Decidability of type checking is proved by an algorithm that first reduces (so, with just beta and computation rules of eliminators), then compares the normal forms in a typed way.

2025-12-02 00:57:19 UTC

- reply

@nprofile…dh59 I was raised in the French school where you define type theory with preterms, a typing relation and a reduction relation and you prove strong normalization in the sense of termination by analogy to rewriting systems. The 2.5 months I've spent so far as a PhD student of Ambrus haven't yet been enough to completely convert me to the intrinsic syntax and semantic normalization proofs point of view 😀

2025-12-02 00:47:03 UTC

- reply

@nprofile…dh59 What do you mean? I'm talking about strong normalization, i.e., termination of reduction, not canonicity. This is what you need for decidability of type checking. And axioms are not a problem there.

2025-12-01 20:42:13 UTC

- reply

@nprofile…adwt Do we even have a proof of subject reduction, confluence, normalization and decidability of type checking for book HoTT?!?!

2025-11-29 22:46:04 UTC

- reply

@nprofile…6fuz Oh, sorry, I had read the post a month ago and misremembered that the feedback was given to the authors and not to the reviewers (fine then).

2025-11-29 22:13:30 UTC

- reply

@nprofile…6fuz Apparently, for STOC 2026, the PC itself is *providing* an AI tool to assist reviewers 😒
https://scottaaronson.blog/?p=9283

2025-11-27 14:44:45 UTC

- reply

@nprofile…v38n Well spotted! LOL. And one of the authors of this bullshit is a apparently a well-known logician, with lots of credentials listed on his Wikipedia page. We live in interesting times, I guess.

2025-11-27 12:29:47 UTC

There's a paper just dropped on arXiv that claims to be able to do some synthetic homotopy theory like in HoTT but with UIP, specifically in Lean…
https://arxiv.org/pdf/2511.19142
using something called “computation paths”:
https://arxiv.org/pdf/1107.1901v3
Has anyone tried to read these and do they actually contain any interesting idea? A very cursory look makes me raise eyebrows; I suspect either it doesn't actually work (I don't see that they are giving a model anywhere) or it can be described in 1 line like “2-level type theory modified in $WAY” but they don't say it.

2025-11-25 10:36:57 UTC

- reply

@nprofile…w8t5 @nprofile…rrqe I learnt Agda without anyone to assist and I picked up the interactive mode usage just fine. I think it was from https://agda.readthedocs.io/en/v2.8.0/getting-started/a-taste-of-agda.html

2025-11-25 03:31:20 UTC

- reply

@nprofile…rrqe We are not going to agree on that one.

2025-11-21 16:59:43 UTC

- reply

@nprofile…v38n I cited your note https://www.danielgratzer.com/papers/2023-semantics-primer-lecture-notes.pdf . Is this link stable? Same question for your book with @nprofile…9t3n.

2025-11-21 16:58:03 UTC

I just created a Wikipedia page "Semantics of type theory". At the moment, it is a stub, containing only the definition of a CwF. I plan to expand it, but by all means do beat me to it.
https://en.wikipedia.org/wiki/Semantics_of_type_theory

2025-11-19 00:19:20 UTC

- reply

@nprofile…stct @nprofile…ztfm Joe proposes a finite list of guesses. Then the game ends and they win if the number was in those guesses. It doesn't continue with more guesses.

2025-11-18 12:07:10 UTC

- reply

@nprofile…ztfm yes

2025-11-18 11:26:26 UTC

- reply

@nprofile…ztfm The original paper (I should have linked it) is this: https://new.math.uiuc.edu/MathMLseminar/seminarPapers/Ben-DavidNature.pdf
It appears to have been published in a conference about… wait for it… AI. 🤷
(And while determinacy is a big source of independence in "normal mathematics", you won't need any of that theory for this exercise, just the well-ordering principle.)

2025-11-18 10:40:09 UTC

- reply

@nprofile…ztfm Since we are chatting, I might as well add tangentially that it is possible to stumble upon independent statements even in recreational mathematics (!). I learnt the following cute example from David Madore:
Consider the following game where Eve and Adam are allied, but cannot communicate aside from agreeing on a strategy in advance. Eve receives two distinct natural numbers and chooses one of them. Adam receives this number and makes a finite number of guesses. They win when the second number was in the guesses.
Easy exercise: exhibit a winning strategy for Eve and Adam.
Now modify the game to replace natural numbers with real numbers.
Exercise: show that Eve and Adam have no winning strategy.
Further modify the game so Eve receives *three* real numbers and chooses *two* of them which are transmitted to Adam. He must make finitely many guesses for the third one.
Challenging exercise: show that Eve and Adam have a winning strategy if and only if the continuum hypothesis holds.

2025-11-17 13:10:19 UTC

- reply

@nprofile…ztfm To be clear, I didn't mean to imply *you* were uneasy with foundations (of course I know that you know a lot more than me about logic), it was just a point about the general perception and status of logic in the mathematical community.

2025-11-17 00:06:38 UTC

- reply

@nprofile…ztfm As a counterpoint, I have a belief (which is hard to substantiate with more than anecdotal facts) that if "generic mathematics" mostly doesn't run into independence phenomena, it is also because "generic mathematicians" more or less consciously *stay clear* of independent statements and more generally anything that requires them to think about foundations, a topic that makes them uneasy.
(Relatedly, I have noticed many times how mathematicians, who usually talk about mathematics with great precision and clarity of thinking, strangely switch to hearsay, vagueness and weasel words as soon as logic is involved.)

2025-11-11 07:16:58 UTC

- reply

@nprofile…kz68 You'll probably also want to watch Andrej's talk at the topos institute: https://youtube.com/watch?v=4CBFUojXoq4

2025-11-11 01:58:04 UTC

- reply

@nprofile…99up I was also wondering: is the problem whether you can make (any flavor of) the Cauchy reals countable still open?

2025-11-10 23:09:53 UTC

- reply

@nprofile…99up Oh right, I've fixed it, thanks.

2025-11-10 22:31:07 UTC

I was asked to give a talk today at our informal type theory seminar in Budapest and chose to present (and hopefully not misrepresent) @nprofile…99up and James E. Hanson's paper on making the reals countable in constructive mathematics – although I 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:
https://jean.abou-samra.fr/talks/2025-11-10-countable-reals.pdf

2025-10-31 20:42:58 UTC

- reply

@nprofile…w8t5 Like we do here with constructive math 🙂 https://mathstodon.xyz/@jeanas/115419702732923188

2025-10-31 16:04:47 UTC

- reply

@nprofile…356e Great! Is the published version identical to the one on arXiv? Otherwise, is it available in open access somewhere?

2025-10-30 15:36:26 UTC

- reply

@nprofile…rrqe What pseudo-scientific viewpoint are you referring to?

2025-10-29 20:50:49 UTC

- reply

@nprofile…ujwf CC @nprofile…0t4k

2025-10-25 20:57:12 UTC

- reply

@nprofile…zemh (Je parle de Ubuntu avec GNOME, pour Kubuntu, i.e., Ubuntu avec KDE, ce ne sera pas GNOME Software bien sûr.)

2025-10-25 20:54:23 UTC

- reply

@nprofile…zemh "Logiciels" probablement ?

2025-10-25 20:30:13 UTC

- reply

@nprofile…zemh GNOME Software (ce truc : https://en.wikipedia.org/wiki/GNOME_Software)

2025-10-22 20:28:17 UTC

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.

2025-10-22 19:10:11 UTC

Agda has an ugly soundness bug when used for UF: it considers the arms of a pattern match to be in a strictly positive position, which looks OK at a glance until you realize that matching on an equality involves transport along an arbitrary equivalence, which is certainly not strictly positive in general. https://github.com/agda/agda/issues/4966
This makes me wonder: has anyone figured out a semantic notion of strict positivity that could replace the ad-hoc syntactic checks used in proof assistants? I mean, UF showed that there are many benefits to using the semantic notion of mere propositions instead of a separate Prop sort with its hacks like subsingleton elimination. I'm wondering if there is something similar here.

2025-10-21 18:51:33 UTC

- reply

@nprofile…rrqe Is Rust on the table? No feelings, just curious.

2025-10-21 14:36:50 UTC

- reply

@nprofile…w8t5 @nprofile…rrqe @nprofile…yqfl Ironically, the first nLab page I looked up something on after this discussion contained total nonsense. (https://ncatlab.org/nlab/revision/diff/Archimedean+ordered+field/33)

2025-10-21 02:37:01 UTC

- reply

@nprofile…lkxk Pierre-Marie Pédrot is visiting us in Budapest and gave a talk about his Dialectica stuff.

2025-10-20 19:26:13 UTC

- reply

@nprofile…lkxk Mathematicians: 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…

2025-10-15 19:28:36 UTC

- reply

@nprofile…yqfl https://github.com/mastodon/mastodon/issues/12423

2025-10-15 19:28:20 UTC

- reply

@nprofile…yqfl Sadly, migrating posts is still not supported 🙁

2025-10-14 11:22:46 UTC

- reply

@nprofile…ujwf Half serious: a temperature?

2025-10-10 08:16:04 UTC

- reply

@nprofile…9gum Dans quel coin ? S'il y a moyen de les récupérer en région parisienne un peu avant Noël, j'y serai de passage et je pars juste après chez ma tante qui est directrice d'école au Liban, dans des conditions rendues très difficiles par la crise économique, que ça intéresserait très probablement.