A new class of philosophically-minded mathematician that I just learned from the logician Paul Levy: smallist.

CH is a statement of third-order arithmetic. It doesn’t quantify over the universe of sets. GCH, on the other hand, does. For smallists, who take a platonic view of PPN (powerset of powerset of the naturals) but not of the universe of sets, this is a big difference. (

I guess it means a mathematician who doesn’t necessarily want in their axiomatic system arbitrary powersets, rather just the few that are needed for ‘ordinary’ mathematics (say up to PPPN, which is plenty to deal with differential geometry, differential equations, functional analysis, number theory, algebraic geometry over number fields or rings of integers therein etc). I think he just invented the word 🙂 but I like it. For a categorically-minded person like me, this means I could work in a pretopos with just a few powersets posited.

(Originally posted to Google+ on 11 November 2016)

MathOverflow question seeking answer, offering bounty

Last year I asked a question titled Direct comparison zig-zag between cochain theories on MathOverflow, and it has still no good answer. I’ve offered a bounty, and no takers yet. The satisfaction is yours for the taking! To quote from the end of the question:

…my hope is to show that the class of cochain theories is connected, assuming one exists, and then exhibit one. This may well be singular cohomology, or it might be something else. In particular I want to remove from the proof of uniqueness the privileged position that any one construction has. The only caveat is that I won’t be able to use any super-sophisticated machinery as this is a first course in algebraic topology. I’m happy to have an outline of how to unwind a sophisticated proof.

Initiality conjecture for full Martin-Löf type theory

Next Thursday, 10th September, Guillaume Brunerie and Peter LeFanu Lumsdaine are going to present a talk Initiality for Martin-Löf type theory in the HoTT electronic seminar … with a proof of the initiality conjecture!

Here’s the abstract:

“Initiality” is the principle that the term model of some type theory should be an initial object in the category of models of that type theory.  Thomas Streicher gave a careful proof of initiality for the Calculus of Constructions in 1991.  Since then, initiality for more complex type theories (such as Martin-Löf type theory) has often been treated as established, as a straightforward extension of Streicher’s result, but never written up carefully for a larger theory.
Around 2010, various researchers (notably Voevodsky) raised the question of whether these extensions really were sufficiently straightforward to consider them established without further proof.  Since then, views on the status of initiality have varied within the field; but the issue has been, at least, a frustrating unresolved point.
In this talk, we present a proof of initiality for a full-featured Martin-Löf type theory.  The proof is formalised in Agda, to dispel any question of thoroughness (and also partly formalised in Coq), and is carefully designed for extensibility to other type theories.  The proof is based on Streicher’s, using some improvements of Hofmann and further refinements by the present authors.  The two formalisations present slightly different versions of the statement — using contextual categories in Agda, categories with attributes in Coq — but the core of the proof is parallel.

Joint work with Menno de Boer and Anders Mörtberg.

This was a big concern of Vladimir Voevodsky and it’s good to finally have it sorted out, with a formalised proof, as it should have.

Unfortunately it’s live at 1am, so I’ll have to grab the recording…

She is asking the right questions


this video makes sense in my head but like WHY DID WE CREATE THIS STUFF

♬ original sound – gracie.ham

Gracie, I can’t reach out to you online, but this is my response as a mathematician. I hope it helps someone.

These kinds of questions you are asking are what drive us as a profession. It doesn’t matter if your example is Pythagoras or whoever. At some point, for every piece of mathematics that we know, someone asked “how?”, or “why?”, or “why not?” and then just let the ideas take them where they would. Literally some of the things that make a stack of technology work came from someone saying “what happens in 3d instead of in 2d?” and then he ended up graffitiing the answer on a bridge when he finally figured it out. No one asked him that question, he asked it himself. No one told him the answer either. It took some hard work, he tried a lot of things, he failed a lot, but he persisted. People had arguments for decades over whether that was the right way to do it. This was 150 years ago. Today I’m pretty sure most 3d animations you see today use that little idea. But he just wanted to know “why?” He wanted to know “can I do it?”

Sometimes it was people just thinking about walking around a town and across bridges. Sometimes it was a fun puzzle. Sometimes it was bets and duels. Sometimes it was a guy who did maths in prison. Sometimes it was a girl who did maths at night when her parents didn’t know and didn’t want her to. But everything we know in maths started with someone asking “why is it like this?”

Please keep asking “how?” and don’t take any nonsense when people don’t realise they don’t know either and never even thought about it.

(Via Jordan Ellenberg via David Butler on Twitter.)

Another good maths journal, this time in analysis

Just as Tim Gowers and co. started the free-to-read and free-to-published journals Discrete Analysis and Advances in Combinatorics, the same platform (Scholastica) has now been used to introduce another such journal: Ars Inveniendi Analytica. Its focus is analysis, and I hope it attracts some big names quickly, to establish its street cred. To quote from the linked annoucement post:

The title of this new journal refers to the term ars inveniendi, coined by Leibnitz to identify the art of discovering new mathematical statements, methods and arguments. This reference aims at highlighting a blooming time for exciting mathematical discoveries in the field of Analysis, and at celebrating the creativity of researchers.

We hope that this editorial enterprise, undertaken in full service of our community, will add up to similar efforts and will encourage the launch of similar operations. Scholars need not only new lines of investigation and new methodologies, but also new and reliable forms for communicating their work. Creating top quality journals, founded and managed by academics, freely accessible to authors and readers, and with minimal management costs entirely sustainable by academic institutions, is the main constructive step that scientist can take to help shaping the future landscape of scientific publishing into something that is more true to the spirit of scientific discovery.

(Apologies if the formatting of this post is weird, I need to get used to the new WordPress online editor.)

Translations of technical words and phrases into French

(UPDATED, SEE AT BOTTOM OF PAGE) With our recent accepted paper, we need to supply a French translation of the title (done), abstract (kinda, with help from DeepL) and the key words. This last one is where I would like any suggestions from francophone mathematicians.

Here’s the list of key words/phrases we need translations of: Whitney extension theorem, smooth functions on closed domain, Whitney jet, polynomial cusps, FrĂ©chet space, submersion, manifolds with corners, manifolds with rough boundary, manifold of mappings, exponential law.

Also, for amusement purposes, here’s the DeepL+ε translation of the abstract:

Cet article examine une version globale et non linĂ©aire du problème de l’extension Whitney pour les fonctions lisses Ă  valeur variĂ©tĂ© sur des domaines fermĂ©s C, avec une frontière non lisse, dans des variĂ©tĂ©s Ă©ventuellement non compacts.
En supposant que C est une sous-variété avec des sommets, ou est localement convexe avec une frontière rugueuse et compacte, nous prouvons que la carte de restriction des fonctions définies partout est une submersion de multiples localement convexes et admet donc des clivages linéaires locaux sur les cartes.
Pour ce faire, nous considĂ©rons la carte de restriction correspondante pour les espaces localement convexes de sections de faisceaux de vecteurs Ă  support compact, nous autorisons le cas encore plus gĂ©nĂ©ral oĂą C ne prĂ©sente que des restrictions lĂ©gères sur les cuspides intĂ©rieures et extĂ©rieures, et nous prouvons l’existence d’un opĂ©rateur d’extension.

I have fixed a few things, like using variĂ©tĂ© for ‘manifold’, rather than the vernacular translation. I would be grateful for suggestions on how to improve it. The original English text is as follows

This article considers a global, nonlinear version of the Whitney extension problem for manifold-valued smooth functions on closed domains C, with non-smooth boundary, in possibly non-compact manifolds.
Assuming C is a submanifold with corners, or is locally convex with rough boundary and compact, we prove that the restriction map from everywhere-defined functions is a submersion of locally convex manifolds and so admits local linear splittings on charts.
This is achieved by considering the corresponding restriction map for locally convex spaces of compactly-supported sections of vector bundles, allowing the even more general case where C only has mild restrictions on inward and outward cusps, and proving the existence of an extension operator.

I’ve had a bit of feedback from various people who know some French and who know how to Google for advice (though no actual French mathematicians—where are you all?), and here’s an updated version:

Nous considérons une version du problème de l’extension Whitney, globale et non linéaire, pour les fonctions lisses à valeur de variétés et définies sur des domaines fermés C à bords non-lisses dans des variétés probablement non compactes.
Supposons que C est une sous-variété à bord anguleux, ou elle est compacte et localement convexe à bords non-lisses, nous montrons que l’application de restriction, à partir des fonctions définies partout, est une submersion de variétés localement convexes, et donc permet des scindage linéaires locaux sur les cartes.
Nous considérons à cet effet l’application de restriction correspondante pour les espaces localement convexes de sections de fibrés vectoriels à support compactes, permettant aussi le cas plus général où C n’a que des restrictions légères sur les cuspides vers l’intérieur et l’extérieur, et montrons l’existence d’un opérateur de prolongement.

And here’s our list of key words:

thĂ©orème de l’extension de Whitney, fonctions lisses sur des domaines fermĂ©s, jet de Whitney, cuspides polynomiales, espace de FrĂ©chet, submersion, variĂ©tĂ©s Ă  bord anguleux, variĂ©tĂ©s Ă  bords non-lisses, variĂ©tĂ©s d’applications, loi de l’exponentielle

Happy to get more comments!

Terry Tao’s first paper: “Perfect numbers”

Terry Tao has just been awarded the inaugural Riemann prize, and as a result I discovered he had his first mathematics paper published at age 8, in a (now defunct) journal for school mathematics in my home state of South Australia. Since this rare item only appears available reproduced as an appendix in a scanned pdf of a 1984 article in an education journal, I thought I’d re-typeset it. So here it is:

Terence Tao, Perfect numbers, Trigon (School Mathematics Journal of the Mathematical Association of South Australia) 21 (3), Nov. 1983, p. 7–8. (pdf)

Note that this appeared 13 years before his earliest listed paper in Math Reviews/MathSciNet.

Edit: I made a GitHub repository for the paper, the LaTeX source, and the code (working, after minor edits) from it. I passed it on to Tao already.

Two Ada books

At the end of last year and beginning of this year I finally read Sydney Padua’s very entertaining graphic novel The thrilling adventures of Lovelace and Babbage about (parallel universe) Ada Lovelace, and then tracked down what seems like the only book on the Lovelace’s correspondence, Ada, Enchantress of Numbers, by Betty Toole.

IMG_20190605_090102 IMG_20190605_120708

The title of the latter is a slight misquote of something Babbage wrote of Lovelace, describing her as “Enchantress of Number”. I have skimmed through the Lovelace–de Morgan correspondence before, painstakingly and faithfully LaTeXed by Christopher Hollings, and was hoping for something in the latter book of a similar nature. Unfortunately all mathematical content is excised. And even some minor typographical changes are pervasive, such as rendering abbreviations like Weddy (for Wednesday) as Weddy. More unfortunate in Toole’s book is the forced analogies that the author tries to make between the conceptual ideas of Ada the person with the design and structure of the Ada programming language. While undoubtedly a thorough treatment of Lovelace’s correspondence would require familiarity with 19th century cultural norms and social history, any examination of precedents of 20th century computer science nascent in the letters to Babbage also requires more than passing knowledge of computer science. Such enthusiastic sections can be safely skipped. But overreaching claims aside, one can see that Lovelace thought deeply about the mathematics she was learning, and how it might be applied to other situations, some rather novel. In the following letter of 1840 she is thinking about how one might mathematically analyse a peg solitare game.


I feel Toole’s book, which consists of chapters of (edited) letters of Lovelace together with explanatory text, lacks somewhat in that one almost always only gets the letters in one direction (there are a few letters from Babbage or de Morgan, for instance, to Lovelace)—unlike the digital Lovelace–de Morgan correspondence. However, at the least, one gets to see the development of Lovelace’s personality from childhood to married life and being a parent while trying to study mathematics, and on to her decline and slow death from cancer. The letters paint a fascinating picture of Victorian Society, whereby mesmerism is seen as a form of medical treatment (though not without some scepticism on Ada’s part against her mother’s urging), and electromagnetism is in the process of being discovered, and mathematics is just about to go through somewhat of a revolution (in the 1830s-40s rigorous analysis was just being established, as was logic as a mathematical discipline). Lovelace’s creativity is surprising, but I would not be surprised if there were periods of real mania, either drug-induced or due to mental health issues. This BBC article notes “At times, Ada certainly had an exaggerated sense of her own destiny. Many of her letters are very long and self-obsessed and often a bit over the top.” Metaphor is used freely and richly, though sometimes it is not clear whether it is fanciful and playful writing or being taken seriously; Toole at times says that Lovelace really did mean the more ‘spacey’ of the descriptions, though it really is not clear. As Stephen Wolfram describes it, some of the letters between Lovelace and Babbage during the drafting and editing of the translation of Meabrea’s article and Lovelace’s attached Translator’s Note read like thick and fast email conversation around modern research (there were of course at the time multiple post deliveries per day, plus servants dispatched with additional letters).

It is this type of modern metaphor that Sydney Padua, freed from the constraints of needing to be historically accurate, plays with freely. The only time the cyberpunk/alternate history asthetic with its modern metaphors feels out of place is in the one ‘real history’ chapter (the opener), where Lovelace goes to tweet about a Babbage party she is at, momentarily mistaking her fan for a smartphone. But once the alternate history starts, the jodhpurs-wearing, pipe-smoking Lovelace is a wonderful character. Padua infuses the writing with a Victorian feel by lifting phrases and dialogue from Lovelace’s and Babbage’s letters, giving pointers when this is done and where they came from, in footnotes. Oh yes, the footnotes. There are footnotes on footnotes. There are pages of endnotes on each chapter, giving real-world historical insight into the fictionalised version. Other historical characters get a look in, such as the engineer Isambard Kingdom Brunel (here seen in the two bottom left panels), or Queen Victoria, whose offer of a variety of knighthood Babbage refused (in real life as in the comic) as it did not come with the honorific ‘sir’.


There is also a lot of historical material in the appendices, including contemporary  articles that Padua sourced by trawling through Google scans of 19th century newspapers. Despite the fictional treatment of the historical characters, one can use Padua’s book at a stepping-off point to find real sources, which she carefully tracked down to inform her fiction, to read more about these larger-than-life personalities.

If only someone would edit a Lovelace–Babbage correspondence and included the mathematics and technical details, and gave informed commentary on the context coming from the history of mathematics at the time….