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.
Remote
Jean Abou Samra (new account)
@jeanas@mathstodon.xyz
mastodon 4.7.2PhD student in theoretical computer science at Eötvös Loránd University in Budapest. Mainly here to chat about TCS/math.
151 Followers
71 Following
30 Posts
Joined February 17, 2024
Pronouns:
he/him
Professional home page:
RE: @highergeometer@mathstodon.xyz
I've heard the same. Let it serve as a reminder that the goals of AI companies are not the same as the goals of the mathematical community.
The Budapest type theory group is hiring a postdoc to work on higher observational type theory.
http://lists.seas.upenn.edu/pipermail/types-announce/2026/012535.html
Replying to
I don't think I know what this means for the future, and I don't think anybody else knows either.
Some of the consequences of the current race to build data centers as fast as possible before we switch to a fully clean grid are unfortunately very well-predicted: just open the IPCC reports :(
I just created a Wikipedia page about cubical type theory. For now this is a stub with just keyword-dropping and reference-dropping. Help to augment it is very welcome, we really need a readable first introduction to cubical type theory written down somewhere.
I'm taking a descriptive set theory course. I'm the only one from the type theory group (which is in the CS department), the others are master's students in the math department. In today's exercise session, one of them wrote on the board “{F ∈ ℱ(X) | F ∩ U}” and said that F ∩ U was a shorthand notation for “F intersects U”. Others started to laugh. He said that after all it makes sense because you can convert a set to a boolean through the function that maps the empty set to the boolean false and non-empty sets to true. After some more amusement, he continued the exercise. I didn't say anything.
Replying to
@jonmsterling Or did you mean congruence of definitional equality and specifically the xi rule / conversion under lambda? Pédrot's paper achieves it, unlike previous attempts.
@mevenlennonbertrand @jpoiret @carloangiuli
Breaking mathematical news: recent events have formally disproved the claim that adults are adults, refuting a nearly 350 years old conjecture of Leibniz. This is the first fully automated contribution to mathematics by autonomous geopolitical agents.
Here's a question I've meant to ask for a long time: https://mathoverflow.net/q/511737/
I added a definition of the effective topos to Wikipedia. I think it's incomprehensible for a newcomer (as it was to me two years ago), but since I ran out of time, pedagogy will have to wait for later or someone else.
Replying to
Replying to
@MonniauxD Non, elle est complètement différente. Les commandes sont écrites sans \ et reconnues au fait qu'elles font plus d'un caractère, et leurs noms sont souvent différents, donc par exemple $forall x, P(x) and Q(x)$ au lieu de $\forall x, P(x) \land Q(x)$. En contrepartie, on n'écrit pas $xyz = 1$ mais $x y z = 1$. De plus, il y a beaucoup plus de raccourcis syntaxiques ASCII. Par exemple, $forall x in RR, x != 0 => exists y in RR, x y = 1$ au lieu de $\forall x \in \mathbb{R}, x \neq 0 \implies \exists y \in \mathbb{R}, xy = 1$.
The setoid model translation takes a model of type theory and returns a new model which validates function extensionality and propositional extensionality for SProp. Has anyone already worked out something like this for unique choice? I guess something like replacing functions with functional relations should work, right? I'm asking because I understand unique choice to be the reason why the definition of the effective topos is so complicated and doesn't just use plain setoids (see the last page of https://arxiv.org/pdf/1307.3832).
Replying to
Replying to
@iblech@mathstodon.xyz Yes, this is precisely what made me smile :-)
Replying to
@jonmsterling I guess I'm illiterate since I often do this sort of silly typo. But more funnily:
Replying to
@olynch@mathstodon.xyz Does this answer your question? https://ncatlab.org/nlab/show/Yoneda+embedding#ReferencesNotation
Replying to
@jhostert The underlying mathematical objects being manipulated are (a specific variety of) cubical sets. But I can't explain much more since one of my purposes in starting this page is to force myself to (belatedly, given my PhD topic) understand the syntax and semantics of cubical type theory sufficiently well to be able to explain this… At any rate, I think that the HoTT book is still the best place to learn about the “types as spaces” interpretation; it will be much easier to understand cubical type theory if you first have a working understanding of the HoTT book (one may hope that eventually there will be introductions to cubical type theory that don't presuppose this knowledge, but that's how it is at the moment).
I also proposed to merge “Homotopy type theory” and “Univalent foundations”. Opinions are welcome on which name to retain…
https://en.wikipedia.org/wiki/Wikipedia:Articles_for_deletion/Homotopy_type_theory
Replying to
(Just in case anybody got misled, this was a pun.)
Replying to
@highergeometer I would love to hear some extremely elementary ∞-category theory. This seems to be a subject in which people rarely explain their intuitions in writing (e.g., why do we define a simplicial set or whichever kind of cubical set exactly like this?).
Replying to
@MadameMollette @bmichel D'après Le Monde https://www.lemonde.fr/politique/article/2026/04/17/sebastien-lecornu-annonce-que-les-boulangers-et-les-fleuristes-pouront-ouvrir-le-1er-mai_6680879_823448.html , il prévoit bien de déposer un projet de loi avant le 1er mai pour remplacer la proposition de loi avortée (restreint cette fois aux boulangers et fleuristes, la proposition de loi d'Attal s'appliquait à d'autres professions), mais il ne compte pas que ce projet de loi puisse s'appliquer pour ce 1er mai. Je crois que l'échéance « avant le 1er mai » est juste une manière de dire « bientôt » sans lien avec l'objet du débat. Par ailleurs, il a effectivement déclaré que « des instructions [seront données afin que] les artisans de ces deux secteurs ne souffrent d’aucune conséquence d’une ouverture le 1er mai 2026 dans les règles fixées par la future loi » et le ministre du travail a clairement dit que les consignes « consistent à ce que les commerçants, le cas échéant, n’aient pas à payer d’amende ».
Replying to
@jonmsterling What do you mean by a “combinatorial presentation of the type theory”? @MartinEscardo @carloangiuli
Replying to
@ncf By “relation”, do you mean a mere relation or a proof-relevant relation?
I have in my mind two conflicting definitions of “f : X → Y has the Baire property (BP)”. (X and Y are topological spaces which I'm happy to assume Polish.) The first is that the preimage of an open subset has the BP (coincides with an open modulo a meager, and open can be replaced with Borel here). The second is that f is “Baire-measurable”, i.e., measurable with respect to the σ-algebras of BP subsets: the preimage of a BP has the BP. Did I dream up that these are equivalent? It comes down to showing that if the preimage of an open has the BP, then the preimage of a nowhere dense has the BP, but I'm stuck on that.
Replying to
@matematiflo@mathstodon.xyz @de_Jong_Tom@mathstodon.xyz @mevenlennonbertrand@lipn.info This looks cool. Do you know how much background will be assumed for Felix Cherubini's synthetic algebraic geometry course? Can I expect to be able to follow, as someone who's familiar with homotopy type theory but not as much as I would like with its semantics, and who knows a few basic facts of algebraic geometry at the level of varieties but doesn't know a thing about schemes?
Replying to
@totbwf@types.pl @ncf@types.pl By the way, how technically feasible would it be to make Mikan translate pattern matching and recursion to eliminators?