Unfortunately, there is no reasonable proof theory for second-order logic with standard semantics. More precisely, there is no deductive system which is simultaneously

- sound — every statement which is provable is valid in all models;
- complete — every statement which is valid in all models is provable; and
- effective — the validity of a proof can be checked by an idealized computer (or an idealized human).

By contrast, first-order logic has all three of these properties.

The undesirable properties of higher-order logic are created by an insufficient notion of model. That is, we cannot have all three, soundness, completeness and effectivness (decidability of proof checking), if we insist that formulas be interpreted in the "standard" set-theoretic way. Henkin semantics does not suffer from this defficiency.

What this says is not that something is wrong with higher-order logic, but that something is wrong with those who refuse to look at semantic models, even when they are right in front of their faces, because these models are "unintended", "philosophically unacceptable", "not what mathematicians think", etc. This phenomenon of refusing to accept new interpretations of old theories is quite persistent, and always very harmful. Didn't someone stall progress in noneuclidean geometry because it was unthinkable that there would be strange new models? Aren't imaginary numbers so called because they were unthinkable and did not "really exist"? Doesn't higher-order classical logic suffer because it is being denied its natural notion of models on the grounds that they are non-standard?

The natural notion of model for intuitionistic higher-order logic (IHOL) is that of a topos. With respect to topos semantics, it is a standard result that IHOL enjoys soundness, completeness and effectivness.

We may specialize this standard fact to classical higher-order logic (CHOL). The result then is that, with respect to Boolean topos semantics, CHOL enjoys soundness, completeness and effectivness. From here on, we may prove various technical theorems which allow us to cut down on the class of Boolean toposes which is stil sufficient for completeness. And then it is not much of a surprise that we cannot cut down just to a single topos known as classical sets, which is called "Paradise" by its prisioners.

Andrej Bauer

A very good interview in French with former Bourbaki members Jean-Pierre Serre, Pierre Cartier and Jacques Dixmier, where the date is given

[Dixmier]: So we have spoken about how we became members [of Bourbaki], let's talk about others. Grothendieck was enlisted as a member of Bourbaki when he was in Nancy.
[Serre]: No, he was not a member of Bourbaki when he was in Nancy, he was a student of a member, that is not the same thing.
[Dixmier]: He was a student of Schwartz and Dieudonné, they said immediately: He is amazing.
[Serre]: Still, this is a very different thing, one did not consider taking him on as a member right away.
[Dixmier]: Well, I would say that he was recruited in 1955, after you [Cartier].
[Serre]: I would say that as well.
[Cartier]: Around the same time.

Dennis Gaitsgory wins the Breakthrough Prize in Mathematics for his central role in the proof of the geometric Langlands conjecture. The Langlands program is a broad research program spanning several fields of mathematics. It grew out of a series of conjectures proposing precise connections between seemingly disparate mathematical concepts. Such connections are powerful tools; for example, the proof of Fermat’s Last Theorem reduces to a particular instance of the Langlands conjecture. These Langlands program equivalences can be thought of as generalizations of the Fourier transform, a tool that relates waves to frequency spectrums and has widespread uses from seismology to sound engineering. In the case of the geometric Langlands conjecture, the proposed one-to-one correspondence is between two very different sets of objects, analogous to these spectrums and waves: on the spectrum side are abstract algebraic objects called representations of the fundamental group, which capture information about the kinds of loop that can wrap around certain complex surfaces; on the “wave” side are sheaves, which, loosely speaking, are rules assigning vector spaces to points on a surface. Gaitsgory has dedicated much of the last 30 years to the geometric Langlands conjecture. In 2013 he wrote an outline of the steps required for a proof, and after more than a decade of intensive research in 2024 he and his colleagues published the full proof, comprising over 800 pages spread over 5 papers. This is a monumental advance, expected to have deep implications in other areas of mathematics too, including number theory, algebraic geometry and mathematical physics.

The proof is huge, almost 1,000 pages. Did you oversee everything in it?

I wrote 95 percent of it. [That was] not for a good reason but because I had an injury from skiing, and I was just lying in bed. So what else was there to do? I was watching Star Wars with my son and writing this thing.

Do you mean you did both at the same time?

Initially, some sections in our papers were named after Star Wars episodes, but at the end, we deleted [that element], mostly out of copyright concerns. But one paper still has a quote from Star Wars: “Fear will keep the local systems in line.” It was a really good fit, because in this paper, we had to control the moduli space of local systems.

[..]

So you hope to catch the interest of young students by teaching them derived algebraic geometry. How did you become interested in the Langlands program in the first place?

It was back in the 1990s, when [Alexander] Sasha Beilinson [a mathematician now at the University of Chicago] came to Tel Aviv [University], where I was a graduate student. Beilinson gave two talks; he was at the very beginning of his own work on the subject. And I was completely captivated. I had learned about the classical Langlands program..., but before his talk, I had no idea that it could be related to geometry. It was the first time I heard about it. The objects he talked about seemed so appealing to me. It was exactly the type of mathematical object that I wanted to study. And they all came together miraculously in this. And I was like, “Wow.” I had to work on that.

Hi Mike. This is what's often called the Density Formula, or (at the n-Lab) the coYoneda Lemma (I think), or (by Australian ninja category theorists) simply the Yoneda Lemma. (But Australian ninja category theorists call everything the Yoneda Lemma.)

I was an nLab holdout for saying that really should be called the Yoneda lemma. Whether you think of Yoneda as saying that hom-bimodules are units for the biclosed structure on bimodules, or for the tensor structure on bimodules -- that's a distinction which doesn't need to be made IMHO, since a unit for one is clearly the unit for the other. But it seems I lost that terminological battle, alas.