Laure Saint-Raymond on the backpage of Libération

There are not many women in the french Académie des Sciences. So it was a great news when last december Laure Saint-Raymond got elected (in the mechanics section, due to her work on physics equations, rather than in the math section).

Today, there’s a portrait of her on the backpage of Libération (a nationwide french newspaper, see picture below). Great exposure for women in science.  And I have noticed that her work has been discussed (in french) in a recent article by her PhD advisor Golse in Gazette des Mathématiciens, while a few months ago there was another portrait of her in Le Journal du CNRS.

(There’s a quite bad typo in the Libération paper: they got the only equation in the text wrong, printing instead of . Sigh…)

Proof assistants and the next decade

It is quite interesting to look, if only casually, at the two trends that are emerging regarding proof assistants:

1) the “natural language” trend: one finds there the work of Ganesalingam & Gowers (which, so far, uses full first-order logic and deals with metric spaces), but also the interesting work of Stovanovic, Narboux, Bezem & Janicic (which, so far, uses a fragment a first-order logic and deals with Geometry à la Tarski). The latter paper discusses the mild differences between these two approaches, and in both papers one can see examples of proofs that these programs produce.   See also Geoproof (maintained by Narboux), for example this nice animation shows a Coq verified interactive proof of Thales’ theorem.

2) the “univalent foundations” trend: Homotopy Type Theory (HoTT),  with these slides by Voevodsky providing a recent account.

All this begs the question: will these two trends merge productively over the next decade? I do hope so (creating a setting with as sound foundations as one would wish for, while ensuring the certified proofs produced are nicely human readable). And in that case, I’m wondering what can be reasonably anticipated.

Probably the gradual emergence of just a big website where mathematicians would write down their proof strategies, which would get accepted or refused in an instant. Obviously, in parallel this would mean the gradual end of some aspects of the technical side of peer-reviewing, but humans would still be left to decide which theorem is/isn’t interesting, which and paper is/isn’t well written.

On a longer time scale, one may envision a time when, with computers just generating indiscriminately all possible theorems by raw enumeration, humans will get completely out the game, and will be left with reading what computers have found. In something like 30 or 50 years time, that’s a distinct possibility.

Summer hiatus

Patrimonio, by Daniel Cremona on flickr