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

[email protected]

Profile Code

nprofile1qqs2skdrfvgp9qwa9u9uh8c6c28gf2q4rwta2qraqvayqu5wc0c9udqpz4mhxue69uhhyetvv9ujuerfw36x7tnsw43qhj6wsd

Publishing to

relay.ditto.pub

Author Public Key

npub14pv6xjcsz2qa6tctew034s5wsj5p2xuh65q86qe6gpegaslstc6qjhtzwd

Show more details

Last Notes

2026-03-27 19:22:02 GMT

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 GMT

- reply

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

2026-02-09 12:25:22 GMT

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

2026-02-08 21:33:35 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- reply

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

2026-01-28 11:24:07 GMT

- reply

@nprofile…xuzd @nprofile…l3hr If you want to distinguish upcasts and downcasts in the syntax, maybe "up <term>" and "down <term>".

2026-01-27 20:48:04 GMT

- reply

@nprofile…mxyk Looks like pure LLM slop to me.

2026-01-25 20:06:35 GMT

- reply

@nprofile…47dl There's @jpoiret.

2026-01-09 15:36:30 GMT

- 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 GMT

- reply

Finally! I've answered the question.

2026-01-07 17:55:05 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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 GMT

@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 GMT

- reply

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

2025-12-27 16:20:03 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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-20 14:03:10 GMT

- reply

I got an answer elsewhere (https://bsky.app/profile/jeanas.bsky.social/post/3mag4c6w7dc2w).

2025-12-20 11:32:22 GMT

Fact: Let A be a commutative ring, let M be a Noetherian A-module and let M₁ and M₂ be two submodules of M. If M₁ ⊆ M₂ and M/M₁ ≅ M/M₂ then M₁ = M₂.
Is this fact obvious to an algebraist (which I am not)? Does it have a name?

2025-12-18 23:17:27 GMT

- reply

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

2025-12-18 23:16:10 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- reply

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

2025-12-06 23:26:34 GMT

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-06 18:08:34 GMT

- reply

@nprofile…w8t5 I don't know, sorry :-) I'm using Typst semi-regularly and I personally like it more than LaTeX, though it has its own flaws of course, but I'm not that much of a power user. Also, I think it really depends on how close to the handwritten version you want the layout to be.

2025-12-06 17:20:37 GMT

- reply

@nprofile…w8t5
(2) For arrows between words, I found this package: https://typst.app/universe/package/pinit
Here is a small test:
#import "@preview/pinit:0.2.2": *
Lorem ipsum dolor sit amet, consectetur#pin(0) adipiscing elit.
Sed id leo ut turpis molestie mollis.
Aenean placerat#pin(1) odio sit amet aliquet convallis. Vivamus ut ligula consequat, tempus orci blandit, euismod turpis.
#pinit-arrow(0, 1)
https://media.mathstodon.xyz/media_attachments/files/115/673/766/920/208/505/original/6579ffad84e7b450.png

2025-12-06 17:08:53 GMT

- reply

@nprofile…w8t5
(1) I've just uploaded the Typst source code to https://jean.abou-samra.fr/talks/2025-11-10-countable-reals.typ
Note that the use of Unicode math characters in the source is peculiarity of mine (I also do it in TeX and elsewhere); most people use the built-in commands and notations, e.g., $not not p => p$ (list on https://typst.app/docs/reference/symbols/sym/).

2025-12-06 15:33:49 GMT

- reply

@nprofile…w8t5 Here's a deck of my own made with Typst:
https://jean.abou-samra.fr/talks/2025-11-10-countable-reals.pdf
It uses the touying package, https://touying-typ.github.io/
I was a bit unhappy that I couldn't just change the theme without also changing other things in the preamble, but other than that, it went rather smoothly.
@nprofile…rrqe

2025-12-03 21:27:16 GMT

- reply

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

2025-12-03 21:18:02 GMT

- reply

@nprofile…yqfl Oh you mean the partiality monad?

2025-12-03 21:08:40 GMT

- reply

@nprofile…yqfl What is the Rosolini lifting monad?

2025-12-03 10:42:38 GMT

- reply

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

2025-12-02 20:54:44 GMT

- reply

It didn't take them long to write another one 🙄
https://arxiv.org/abs/2512.00657

2025-12-02 01:04:26 GMT

- 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 GMT

- 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 GMT

- 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-02 00:24:54 GMT

- reply

@nprofile…adwt Oh wait, I guess we should be able to get it from the fact that book HoTT can be encoded into plain MLTT with inductives using the "Licata trick" https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/

2025-12-01 20:42:13 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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 GMT

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 GMT

- 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 GMT

- reply

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

2025-11-24 22:10:24 GMT

- reply

@nprofile…d7hz "decidably pointed" is what I would've come up with.

2025-11-21 16:59:43 GMT

- 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 GMT

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 GMT

- 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 GMT

- reply

@nprofile…ztfm yes

2025-11-18 11:26:26 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- 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 GMT

- reply

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

2025-11-10 22:31:07 GMT

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-11-07 10:28:47 GMT

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.
https://arxiv.org/pdf/2511.03752

2025-11-03 16:59:34 GMT

- reply

@nprofile…w8t5 A mathematician I know will die on the hill that because the equality in univalent foundations doesn't have the expected properties, it doesn't deserve to be called equality. Which I'm sure you would disagree with 🙂

2025-11-02 15:02:36 GMT

- reply

@nprofile…rrqe Wait, what makes you *accidentally* get multiple cursors in Helix? (I'm using it daily and this never happens to me.)

2025-11-02 13:28:07 GMT

Random trivia bit that I cannot figure out from the Internet. Is "univalence" pronounced as you-*knee*-val-n-s or you-knee-*vay*-l-n-s? What about “univalent”?
On https://www.howtopronounce.com/univalence there are recordings going both ways…

2025-11-02 11:53:40 GMT

- reply

@nprofile…aamk I'm ashamed to admit it, but:
It holds in an arbitrary commutative ring (no assumptions like being a domain) that if a and b are not units then ab is not a unit.
(After I did the proof, I concluded that this was the right time to stop my work day.)

2025-10-31 20:42:58 GMT

- reply

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

2025-10-31 16:04:47 GMT

- 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 GMT

- reply

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

2025-10-29 20:50:49 GMT

- reply

@nprofile…ujwf CC @nprofile…0t4k

2025-10-25 20:57:12 GMT

- 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 GMT

- reply

@nprofile…zemh "Logiciels" probablement ?

2025-10-25 20:39:48 GMT

- reply

@nprofile…zemh s/Linux/tout/ ?
À un moment où je m'étais mis en tête de contribuer au site de documentation sur le packaging Python, je me rappelle de questions « votre doc dit de faire ça, mais sur cette réponse StackOverflow d'il y a 7 ans, je trouve autre chose, quelle est la bonne méthode ? ».
Il y a plein de problèmes qui se superposent :
(1) les gens n'aiment pas lire la doc, mais aussi
(2) la doc est souvent merdique voire inexistante, et on s'est structurellement habitués à ce que ce soit la normalité, et
(3) quand elle est détaillée, elle est au contraire trop technique pour le néophyte (rares sont les logiciels qui ont une doc introductive accessible ET une doc technique détaillée),
(4) les gens écrivent des choses dans leur propre doc au lieu de pointer vers la doc canonique (“voici les instructions pour installer bidule <commandes qui ne marchent que sur une config et sont obsolètes deux ans plus tard>” au lieu de “voir <lien> pour les instructions officielles sur l'installation de paquets en $LANGAGE”),
(5) le Web est saturé de sites à la con optimisés en SEO qui veulent te faire regarder un maximum de pub avant de trouver ta malheureuse commande, et maintenant d'AI slop.

2025-10-25 20:30:13 GMT

- reply

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

2025-10-23 13:57:32 GMT

- reply

@nprofile…w8t5 @nprofile…yytj @nprofile…rrqe While answering a StackExchange question I needed to remember how this proof worked, and I just followed my nose without really thinking and ended up with this proof 🤷
I mean, you have the ML eliminator of type
(P : (x y : A) → x = y → 𝒰) → ((x : A) → P x x refl_x) → (x y : A) (p : x = y) → P x y p
and you want to prove the PM eliminator of type
(x : A) → (P : (y : A) → x = y → 𝒰) → P x refl_x → (y : A) (p : x = y) → P y p
The only idea (?) is to reorder the arguments (!) as
(x : A) (y : A) (p : x = y) → (P : (y : A) → x = y → 𝒰) → P x refl_x → P y p
which has the shape of the conclusion of the ML eliminator. Applying it, we are reduced to proving (P : (y : A) → x = y → 𝒰) → P x refl_x → P y p with y :≡ x and p :≡ refl_x, for which the identity works.

2025-10-22 20:28:17 GMT

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 GMT

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 GMT

- reply

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

2025-10-21 14:36:50 GMT

- 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 GMT

- 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 GMT

- 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 21:43:19 GMT

- reply

@nprofile…rrqe @nprofile…yqfl As someone who's been there: a thousand times yes.
Somewhere deep on my TODO list, there is writing Wikipedia pages on 2010s type theory like "Univalence axiom" and "Cubical type theory" (I already started "Uniqueness of identity proofs" a while back). Of course, I only get 24 hours a day…

2025-10-15 21:19:30 GMT

- reply

@nprofile…w8t5 @nprofile…rrqe @nprofile…yqfl I read few nLab articles about things I'm familiar with, so I can't really judge it, but I can imagine several explanations to this:
One is that there are just a lot more people editing Wikipedia. For comparison, I completely stopped reading math articles on the French Wikipedia because they're often much worse, and judging by article count French Wikipedia is "only" ~2.5 times smaller than English Wikipedia.
Another is that Wikipedia strongly enforces "no original research" and "everything must be sourced". In particular, even a mathematical proof doesn't replace a citation (this is explicitly written in the guidelines). nLab has few inline citations and encourages contributors to adopt the "nPOV" (categorical/higher-structures/…) in the articles, rather than merely synthesizing the main reference works on a given subject as they are written by people who don't take this point of view.

2025-10-15 19:52:05 GMT

- reply

@nprofile…ujwf @nprofile…yqfl Yes, you can still access it. It's "frozen" in the sense that the profile page has a message directing to the new account and you can't post anymore, but you can easily unfreeze it and use it again. I recently did exactly this, going back to my old mathstodon.xyz account (this one) after the epic fail where I accidentally deleted simultaneously my own Mastodon server's database and its backup…

2025-10-15 19:28:36 GMT

- reply

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

2025-10-15 19:28:20 GMT

- reply

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

2025-10-15 18:43:13 GMT

“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. Now I have to sit for half an hour and to prepare my lectures now and then (thanks God this concerns only advanced graduate courses yet). And I work as a professional mathematician in academia full time!”
— https://mathoverflow.net/a/143317/
Cough cough. Can anyone please reassure me that it's okay to need time to prepare your lectures/tutorials when you're just a normal human being?

2025-10-14 11:22:46 GMT

- reply

@nprofile…ujwf Half serious: a temperature?

2025-10-12 21:59:59 GMT

Psst, topologists (cc @nprofile…hszg @nprofile…l9jz)
I've just finished a complete overhaul of the Wikipedia page on filters:
https://en.wikipedia.org/wiki/Filter_on_a_set#Filter_bases
(compare with the previous version: https://en.wikipedia.org/w/index.php?title=Filter_on_a_set&oldid=1310480672)
What do you think of the page? Does any missing information come to mind (that should go into this article rather than adjacent ones like “Ultrafilter” or “Filters in topology”)?

2025-10-10 08:16:04 GMT

- 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.

2025-10-09 12:03:42 GMT

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.
https://www.mediawiki.org/wiki/Requests_for_comment/Mobile_domain_sunsetting/2025_Announcement

2025-10-07 19:04:26 GMT

- reply

@nprofile…nauq What you call the n-truncation of Type I'd call the type of homotopy n-types.

2025-10-07 19:02:34 GMT

- reply

@nprofile…nauq I think what people usually mean by the (-1)-truncation of T : Type is the propositional truncation, ||T|| in the notations of the HoTT book, a.k.a. bracket type [T]. (For example: https://ncatlab.org/nlab/show/truncation) This is the higher inductive type defined by the constructors mk : T → ||T|| and trunc : Π (a b : ||T||) ⋅ a = b.

2025-10-07 18:36:03 GMT

- reply

@nprofile…nauq @nprofile…6kk0 Yes, “hprop” (homotopy proposition) and “mere proposition” are synonyms. (But what do you mean by “Prop is the (-1)-truncation of Type”?)

2025-10-01 21:32:23 GMT

- reply

@nprofile…hszg Are there recordings or slides available somewhere? The list of abstracts is tantalizing.

2025-10-01 19:30:07 GMT

- reply

@nprofile…6kk0
> did I mention I’m using Swift?
For Pterodactyl? Didn't you mention Lean in your talk?