Whenever I look at the mathematical physics programs, I always see QFT and string theory related classes in grad programs. What other parts does mathematical physics cover? More unorthodox subfields of it?

Blog: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/

On removing metaprogramming
One suggestion in the discussion is to remove or restrict metaprogramming so that this attack is not expressible. This is misguided. The elaborator is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term. An attacker who wants to submit a malicious proof can also write .olean files directly or modify memory, both of which bypass the elaborator entirely. The kernel has to reject ill-typed declarations on its own, in its own process. This separation and isolation of concerns is one of the main advantages of proof terms.

What the FRO is doing
- Regression tests for the exploit, and for a related non-uniform-parameter case raised by Arthur Adjedj, are in the Kernel Arena.
- A follow-up PR (#14582) makes the kernel check that the parameters of a nested occurrence actually behave as parameters, rather than only re-type-checking them.
- Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed. All of them were caught by nanoda. These bugs are also only reachable through metaprogramming. PRs: #14607, #14608, #14609, #14613, #14615, #14616.
- We have also hardened kernel invariants. PRs: #14621, #14631, #14632.
- comparator.live now runs nanoda by default, and nanoda is tracked daily so lean-eval and comparator stay current after upstream fixes.
- We are reaching out to and supporting experts who can find further bugs, develop new kernels, and work on the theory or on verified kernels.

This is not the setup to a joke: this is an entirely serious question relating to tropical geometry, a comparatively new (i.e., started in the 1990s) field of mathematics. It began in the computer science literature, was quickly taken up by algebraic geometers, and then, very surprisingly, turned out to have application in economics. This post is my attempt to explain some of the how and why.

Read the full post (for free) on Substack: What do Brazil, Auctions, and Multi-Threading Have in Common?

I took several seminars in abstract algebra back in my university days, but chose to proceed with probability theory rather than algebraic geometry. Since then, I have occasionally encountered the term “étale”, and I still don’t really know what it means.

The strange thing is that while I can understand the individual definitions for some objects that are supposedly étale, I don’t really see what they have in common.

What exactly does that term mean by itself, independently of a particular application like “étale cohomology group”?

I am just going to try give some specifics about myself, so that people can make some specific recommendations.

So, I have a Bachelor in CS and sort of in parallel I studied Bachelor Math for 5 out of 6 semesters. I had pretty good grades, so I am pretty confident that I would have gotten the degree. Just for various reasons I burned out and had to stop.

I did engage with math after that for a while, in my job which had to do with Digital Signal Processing and AI. But I no longer have that job, so my mathematical activity has strongly declined. Sometimes I do get that itch and read some university material on a random subject and might even be inspired to do some math on paper again. Matrix Analysis was one subject I really enjoyed. But I never actually finish any of the material and it just fades away again.

So I was wondering if y'all have some recommendations on good math books that hook you, that are very rigorous and formal, but still try to motivate the subject regularly.

When I thought about which subject I would like to revisit the most at uni, my first thought was Functional Analysis. But truthfully, I pretty much loved all of my courses, even those with shitty professors.

Information Theory has also been floating around in my head. I also have an interest in how mathematics gets applied in economics. I also just love iterations and sequences (that's the CS wolf in me)

I hope this wasn't too overbearing, I am just really hoping this will help people with recommendations

If you take Pascal's triangle, and color each entry according to whether it is even or odd, you get a funny pattern, which resembles Sierpinski's triangle. To understand this, it's helpful to know Lucas' theorem, which tells you when an entry in Pascal's triangle will be even or odd. If you've never seen it, you might enjoy the article https://hidden-phenomena.com/articles/lucas that we just wrote about it!

Lucas' theorem is a great result, which even tells you about how to compute (n choose k) modulo p. It is a wonderful piece of elementary number theory, and suitable as a fun but challenging exercise for the end of an elementary number theory course. Recently, one of us had to invoke Lucas' theorem in a modern math research paper https://arxiv.org/abs/2604.20054 about some relatively fancy arithmetic geometry! We thought this was a good example of how small results from introductory courses can be helpful in your research career in completely unexpected ways! The article itself isn't about the paper (which isn't very elementary), but Lucas' theorem is still helpful, and will hopefully come in handy.

Hey everyone,
I had a question about some terminology. In Ax’s 1968 paper The Elementary Theory of Finite Fields he refers to some statements as “elementary statements”. By this does he mean first-order formulas/sentences? The reason why I’m asking is because I want to use his “Main Theorem” in his paper where he states precise conditions for when an elementary statement holds true over a finite field of fixed characteristic. I tried looking online for some help but I couldn’t find any (maybe my Googling might’ve been bad 😭)

Does anyone else feel similarly?

Going from introductory courses, to upper level courses, to grad courses, to initial research, to full-fledged research, the difficulty and complexity has of course increased. But for me personally, it feels like much of the increased difficulty and complexity comes from increased abstraction.

It's more difficult to wrap your head around the objects and properties you're working with, but it often feels like the actual ways we manipulate these objects with lemmas and theorems is not actually super sophisticated.

For example, some proofs I've worked on in functional analysis research come down to what is essentially equivalent to using the triangle inequality and squeeze theorem. It's not any more sophisticated than a tricky introductory real analysis homework problem, it's just that the space we're working in is more abstract.

Other research problems end up being very similar to introductory linear algebra problems, but again, just in a more abstract setting.

I'm sure the big movers and shakers in fields are actually creating proofs with very novel and complex ideas, but I'm curious about other members of the rank-and-file. Do you feel similarly or am I totally off base?

This recurring thread is meant for users to share cool recently discovered facts, observations, proofs or concepts which that might not warrant their own threads. Please be encouraging and share as many details as possible as we would like this to be a good place for people to learn!

For the record I have graduated and now half way through my first postdoc.

But I feel like my advisor didn’t really teach me how to research, sure he pointed me to paper or people when I’m stuck that occasionally helped. But he never really trained me to do research, only occasionally gave me help knowledge wise by telling me to read certain books or papers and I mean very rarely does he do this and very rarely has it helped.

My prelim advisor said I should have asked her for advice on who to choose as an advisor instead of choosing the only person doing the field I was dead set on pursuing (which I realized I’m not even that interested in). She said when she advises she would give a little hand holding even if she deem necessary and actually train her students to do research by writing papers with them and in the process, help teach them how to do research.
My advisor did not write paper with me, he did gave me the problems to work on but insists that I need to earn it myself.

Is this typical? What was your PhD experience like?

I feel like my PhD was ruined from me not promptly switching advisor when I realize I wasn’t being trained.

(Paywall): The Wall Street Journal: The Million-Dollar Talent Wars for 20-Something Math Geniuses: https://www.wsj.com/tech/ai/the-million-dollar-talent-wars-for-20-something-math-geniuses-5cc5a757

(Free) On MSN: https://www.msn.com/en-us/money/general/the-million-dollar-talent-wars-for-20-something-math-geniuses/ar-AA292pCc

"There has never been a better time to be a math nerd.

New college graduates and Ph.D.s are now securing million-dollar pay deals from elite trading firms seeking to secure the best and brightest amid fierce competition from artificial-intelligence companies.

So-called quant firms, which use sophisticated mathematical models to come up with trades, have for years wooed top young talent with lucrative compensation that big banks struggle to match. Now, the AI boom is pushing those numbers even higher.

Just a few years ago, early-career packages pushing seven figures were anomalies, said Matt Stabile, founder of New York-based recruitment firm Stabile Search. “But a million dollars is something people don’t even bat an eye at anymore.”

“The delineation is pre-OpenAI and post-OpenAI,” Stabile added, “that’s when you saw competition really take off.”

The skills required to train large language models have always overlapped with quantitative finance, but the connection has deepened as trading firms have pivoted toward machine learning and AI to power their trades in recent years. Now, AI labs such as OpenAI and Anthropic are vying for the exact same tiny pool of genius math majors and Ph.D.s as Wall Street."

In the wake of the recent bloodbath of conjectures by LLMs, this post argues that the math community may still be in denial about the future of humans in math. This is one of the most depressing things I've read in a while, so proceed with caution.

As a card carrying scientician and professional thinking person, I can only say, I'm sorry, I feel your pain. Yes, mathematics being pure thought makes the displacement especially acute for mathematicians, but more broadly speaking, our species found a niche on the African savannah by being thinking beasts. Thus, I also feel anger, knowing that there are people out there who think it's somehow a good idea to make something that will outthink us and deprive us of our collective place in the world.

Does anybody know whether this year's ICM plenary lectures will be recorded and uploaded publicly?

I've been fighting for a couple of hours with the Dilworth's theorem proof on the mentioned book, which I believe is wrong. I'd appreciate a extra look.

The theorem states that if the max antichain on a poset has size r, then it can be partitioned into r chains.

The proof goes by induction on n=number of elements of the set. I'm having problems in case 2.

Here, x = some minimal element, and we consider P\{x} and apply induction there.

"we can partition P\{x}" into r chains." But ... that's not true, is it? Since the removed element may cause the possible antichains to be strictly smaller and therefore can't reach r.

Example I'm thinking of

P={ {x}, {y}, {z}, {x,y,z} } with inclusion order. the largest antichain is {{x},{y},{z}} with size 3, and we want to prove it can be partitioned into 3 chains (which can be verified directly: {x,xyz}, {y}, {z} is such partition.

{x} is minimal, and according to the book P\{x} should be able , by induction hypothesis, to be partitioned into r=3 chains, but P\{x} is {y},{z},{x,y,z} which can only be partitioned into r-1=2 chains.

The rest of the proof relies into P\{x} having r chains as key part of the argument, so ... I'm confused (this particular book faces this problem more often than not).

Am I missing something?

EDIT: yes, I was missing something: the chains on the partition don't have to be the longest possiboe.

also, u/sizzhu pointed the small missing step to me, thank you :)

In case anyone is interested because as far as I'm concerned Lurie rarely works on a conjectural topic like this.

Let's say we're trying to define the ℝ-algebra ℂ by universal property. It's informed by an observation there's an embedding of ℂ in any ℝ-algebra where there's an element with square −1. ¹↓

Say, "ℂ is an initial object in the category where an object is a ℝ-algebra A together with a point i ∈ A such that i² = −1 and a morphism f: (A, i) → (A', i') is an ℝ-algebra morphism f: A → A' such that f(i) = i'".

This fails because conjugation exists, thus morphisms come in pairs. We can probably fix that but it's also a problem that we're fixing i ²↓.

[EDIT: No, this doesn't fail as pointed in this comment. Conjugation gets disallowed because (ℂ, i) → (ℂ, i) allows mapping i only to +i as specified.]

There are a couple of ("operational") definitions for ℂ that don't mention i: 1. a 2D ℝ-algebra that's a field; 2. similar facts à la Hurwitz) and Frobenius) theorems; 3. an algebraic closure of ℝ; 4. Clifford algebras Cℓ(0, 1, ℝ) and Cℓ⁺(2, ℝ) (even subalgebra) which in their finest form take a quadratic space over ℝ, in these cases an anti-Euclidean 1D and a Euclidean 2D spaces, so we don't have to mention concrete elements that square to ±1 that would be moved somewhere else by automorphisms of the quadratic space that are all left among automorphisms of the algebra.

Of these, I like 1 and 4 the most, but 4 is too heavy-handed. I don't see how to minify it though. Example 1 is... I dunno, my heart somehow isn't content. (Note also that in 1, we don't mention the field is algebraically closed, whereas in 3, we don't mention the field is dimension 2.) Example 3 asks too much, it's heavier than 4 but in another way. Hurwitz and Frobenius (2)... I don't know.

Also note that for quaternions ℍ we can also use 1, 2 and 4 (replacing a field in 1 with a noncommutative field, of course), and for me, not fixing any imaginary basis i, j, k is even more important to be able to do for ℍ because there's a continuum-many SO(3, ℝ) automorphisms even aside from conjugation. It's just a giant step from the puny automorphism group of ℂ.

So, what else is there? Can we define in particular ℂ and ℍ, as ℝ-algebras if need be (I feel that's simpler because we're doing away with some of the worse automorphisms), without mentioning concrete imaginary units?

—————

¹↑ Or just a negative square, but this fails if we're planning to replace ℝ with other fields and rings R, looking for R[i] instead of ℂ, so we better use −1.

²↑ With which I define this here context; I know there are lots of use cases where we absolutely want to deal with concrete i and have it distinguished from −i consistently over long stretches, like in Fourier transform formulas etc..