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

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

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

Please help me list math formalization projects looking for volunteers: mathoverflow.net/a/500723/

This is a great read on the attacks on Wikipedia over alledged bias: 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 ℤ = ℤ.

I have a basic question about set theory. When are ⟨V_α; ∈⟩ and ⟨V_β; ∈⟩ elementarily equivalent?

@pianocktailiste.bsky.social Donc, tu disais que sur la Wikipédia française les pages de maths sont imbitables mais que sur l'anglaise elles sont mieux ? Permets-moi de te présenter : en.wikipedia.org/wiki/Constru...

Is Agda a homage to Henk Barendregt?

On my blog: a rant on the nonsensical IT security advice I receive jean.abou-samra.fr/blog/securit...

Let me just drop this link here since, as an apprentice type theorist, I managed to miss this incredibly interesting and important paper: arxiv.org/abs/2009.12670 (If you were wondering, the chances that I will soon be able to read a 200-page paper full of heavy ∞-category theory are zero.)

Browsing math.LO on arXiv, I see a paper marketed as a simplification of type theory to make it more appealing to pure mathematicians. If anyone read it, does it contain anything interesting? From a cursory glance, it looks heavily misguided, but I didn't go deeper.

I wrote an op-ed on the world-class STEM research ecosystem in the United States, and how this ecosystem is now under attack on multiple fronts by the current administration: newsletter.ofthebrave.org/p/im-an-awar...

This crank paper that I was linking for fun last year has been published in a Springer journal 😱 blog.computationalcomplexity.org/2025/08/some...

Ooh but this one beats it hollow: www.preprints.org/frontend/man... (via mathstodon.xyz/@highergeome...)

Most wicked type theory soundness bug I've seen to date: github.com/agda/agda/is...

Hartmanis-Stearns conjecture: If the expansion of a real x in some base b ≥ 2 can be written by a multitape Turing machine with bounded time intervals between the successive digits… then x is rational or transcendental!

I'm very sad to hear the news that Gilles Dowek has lost his battle against cancer, aged 58. He was a professor of theoretical computer science at ENS Paris-Saclay. His major scientific work was to develop the theory of the λΠ-calculus modulo, a type theory built from user-defined rewriting. (1/3)

Here's a new Wikipedia page on the TheoretiCS journal: en.wikipedia.org/wiki/Theoret... Feel free to improve!

I wrote a long-winded MathOverflow answer about universes in type theory mathoverflow.net/a/497615/ . I hope I didn't talk nonsense too much…

I found this paper amazing: "Fusible numbers and Peano Arithmetic", by Jeff Erickson, Gabriel Nivasch and Junyan Xu, LICS 2021, arxiv.org/abs/2003.14342 A popular riddle asks: Given two fuses each of which burns for an hour, how to measure 45 minutes?

I am officially a fringe computer scientist. mathstodon.xyz/@MartinEscar...

I asked a MathOverflow question about p-adic valuations in a sequence of vectors satisfying a holonomic-like recurrence relation. My research team is pretty much stuck on this; I wouldn't be surprised if there was a rather simple trick, but we can't see it so far. mathoverflow.net/q/497090/519...

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?

How do you call in English the basic identity k⋅binom(n, k) = n⋅binom(n-1, k-1) ? I was taught this under the name “the captain's formula” in my first year of university (it's the number of ways to choose a team of k members from n people and a captain from that team).

Does anyone here know about p-adic differential equations? A colleague and I would appreciate references: mathoverflow.net/questions/49...

The following computability question looks perfectly innocuous but has me stumped: Define a “separation problem with promise” to be a triple (P, L, R) where L ⊆ ℕ and R ⊆ ℕ are disjoint and P ⊆ ℕ is a superset of both. (1/5)

Wikipedia gives the following example of a directed preordered set on en.wikipedia.org/wiki/Directe... : Given x₀ ∈ ℝ, endow ℝ∖{x₀} with x ≤ y :⇔ |x-x₀| ≥ |y-y₀|. I don't get the point: that's just (ℝ, ≤) with each point doubled. Does anybody have an idea in which context this is a natural example?

Start your engine 🏁 Our new WikiRun online game pits you against a daily speed race. Your mission is to go from the start article to the end article by racing through Wikipedia from link to link – to the finish line. WikiRun is available until 4 July, so you better run ➡️ wikirun-game.toolforge.org

I remain impressed with Agda. Yesterday, in response to a riddle posted by Martín Escardó (mathstodon.xyz/@MartinEscar...), I was nerd-sniped to formalize my answer (gist.github.com/jeanas/56ea8...).

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?

As I read a paper touching upon that area, I'm beginning to think algebraic number theory is even more confusing (and, unlike type theory, needlessly so). “The integer √2” “Let x be a rational integer and p a rational prime” “In the field K, the factorization of ideals into prime ideals…” etc.

J'allais me moquer du Figaro pour cet article qui présente les conclusions de géobiologues comme des faits alors que la géobiologie ( fr.wikipedia.org/wiki/G%C3%A9... ) est une pure pseudoscience et ces histoires de rivières souterraines sont des foutaises. www.lefigaro.fr/actualite-fr...

Not sure how I missed this, but Dijkstra's algorithm has been beaten on sparse graphs 😮 arxiv.org/abs/2504.17033 (Unsurprisingly, this got a STOC'25 best paper award.)

This is one of the funniest crackpot papers I've seen: arxiv.org/abs/2505.21038

I wrote a Mastodon thread with some opinions about formalized mathematics: mastodon.abou-samra.fr/@jeanas/1145...

Thinking about this MathOverflow question mathoverflow.net/questions/49... makes me wonder: what's a slick proof that there are 2^κ *non-isomorphic* (simple undirected) graphs on κ vertices for infinite κ? I can prove it, but in a slightly ugly way. What would be your solution?

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:

I just wrote: “We use the notation π₁(p) and not π₁ p to stress that π₁ is not an actual function.” Am I being too sarcastic to mathematicians?

This paper figshare.com/articles/pre... was advertised in a MathOverflow “question” (now deleted by moderators). On first sight, from my perspective as an outsider to set theory with some basic notions of it, the paper looks undistinguishable from a legit set theory paper.

“Frankly, Jean, you're paranoid to outright dismiss possible PhD positions in the US. Nothing bad is going to happen.” www.bbc.com/news/article...

A really silly question about English: sometimes I see “Doe's theorem”, sometimes “the Doe theorem”, e.g., Wikipedia says “Brouwer fixed-point theorem” in the title on en.wikipedia.org/wiki/Brouwer... but “Brouwer's fixed point theorem” in the lead sentence.

An interesting point of view on Lean (I don't know if I agree but it's interesting in any case): mathstodon.xyz/@jonmsterlin...

In simply typed λ-calculus with product/sum/unit/empty types, if u : A + B in the empty context and u is normal, it must have the form ι₁(v) or ι₂(v) by canonicity. What's the quickest proof that this remains true in a context where all types are variables?

Looks like Steve Awodey just published a paper on a variant of toposes more closely suited for MLTT: arxiv.org/pdf/2505.10761 (Via mathstodon.xyz/@MEvans/1145...)

Je dois coûter presque 100k€/an en superbrut à mon université et personne ne vérifie si je fais mon travail. En revanche, pour 5 balles, la chaîne de validation est délirante. 1000 euros à tout casser par an. Ce système est fou.

This is, apparently, an actual commutative diagram excerpted from an actual math paper. (Seen on mathstodon.xyz/@highergeome...)

@gro-tsen.bsky.social Do you know any propositional formula φ⇒ψ where converting a realizer of φ to a realizer of ψ is possible platonically but requires 0'' computational power? I see examples which need 0' (e.g. Scott) and others where a PA degree suffices (e.g. Kreisel-Putnam) but nothing higher.

Your periodic reminder that the confidence in a formalized proof is bounded above by the confidence that the formalized statement matches the informal statement. github.com/SystymaticDe...

James Hanson's MathOverflow answers never fail to fascinate me. Here, on separating the internal logics of sheaf toposes over topological spaces from those over locales… using the continuum hypothesis: mathoverflow.net/a/492256/519...