aureianimus

I concur with one of the other replies: very few or none.

This is putting the cart before the horse: Progress in verification has been huge because of LLMs. Mathlib PRs spiked at the release of Opus 4.6, any of the big formalizations would not have been here without LLMs.

More surprising to me, OpenAI claims they're doing informal reasoning and only after do the formalization. This seems to match the way in which they release things. Of course they will have Lean in the training data, but I think this supports the mirror hypothesis: We'd have the same progress in mathematics if proof assistants didn't exist, it would just be a pain to verify correctness.

Fully agree on the potential for Lean as a generic programming language.

The thing is that Navier-Stokes has a definition split off separate from the formalization, and that is what has been completed. People have looked at the definition of the final statement. This paper only mentions the proof and intermediate statement, not the final statement. The most likely case to me is that intermediate statements do not match, but the end result still holds.

I was at the workshop that resulted in the Leiden Declaration in Fall 2025. The majority vibe was that this was inevitable, but hard to predict whether it would be in one year or 30 years.

The thing is that there is a standard format where the definition of the theorem is split from the proof, and verifying that the definition matches the mathematical concept is a LOT less work then reading the proof, especially if you're willing to assume that definitions in Mathlib are correct.

There's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running this tool indeed reduces the correctness question to what the parent comment mentioned.

To give a more precise indication, I watched maybe the first 5 minutes of lecture 1 and 5 for this.

I highly encourage you to take "didicatically useful" as a bar to aim for, rather than "not making mistakes".

I think it's a cool tech demo, but if you're positioning this as a course that's ready to be consumed by students, I think doing the quality control is not optional.

I watched some snippets, and would like to put forward some points in support of the former:

- The voice is clearly TTS, which I think really loses something. Not having variation or stressing particular parts with intonation is a big deal in teaching. The beginning of lecture 5 has a pause in a weird spot (surface).

- The intro to the first lecture is already unnatural: "And that's of course now we're going to start working with functions of more than one variable."

- The scaffolding in lecture 1 is off to a bad start. The lecture tries to rope the student in with a question, but the question uses the notion and notation of a vector that has not been introduced yet. This reeks of a prompt "use a (motivating) question to introduce the topic", but a question that cannot be understood by a student does not help.

Graphlib? Do you have a link to this for me?

I have this with my phone, but it's because of dust. Did you try cleaning the port?

With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.

The version I heard involves a 3d artist adding an obnoxious fairy flying around the character, so not critical, but noticable.

I also think the idea here is to apply it to bosses who's self-worth seems to be tied to putting their mark on the product without being burdened by knowledge. (Because they'll want to change something regardless of the state)