aureianimus

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.

Very cool! It seems you've got a great setup. An addition that would be very convincing is going the extra mile and making a comparator setup for your Lean proofs. (https://github.com/leanprover/comparator) This ensures that the AI is not, in any way, modifiying the Lean context in ways that could lead to unsoundness.

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)

All the good resources are listed here: https://lean-lang.org/learn/

I recommend the natural number game (also mentioned above) for a casual introduction to the mathematics side, just to get a feeling.

If you are serious about learning lean, I recommend Functional Programming in Lean for learning it as a programming language and Theorem Proving in Lean for learning it as a proof assistant

I think the difference is mostly cultural. The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.

Many people in the Rocq community see this as a no-go and some argue this will cause the system to be hard to use over the long run. In the Lean community, the interest in type theory is at a much lower level, and people see this as a practical tradeoff. They recognize the theoretical issues show up in practice, but so infrequently that having this axiom is worth it. I consider this matter to be an open question.

If you look at what's being done in the communities, in Lean the focus is very much on and around mathlib. This means there's a fairly monolithic culture of mathematicians interested in formalizing, supplemented with some people interested in formal verification of software.

The Rocq community seems much more diverse in the sense that formalization effort is split over many projects, with different axioms assumed and different philosophies. This also holds for tooling and language features. It seems like any problem has at least two solutions lying around. My personal take is that this diversity is nice for exploring options, it also causes the Rocq community to move slower due to technical debt of switching between solutions.

In a lot of cases you can get far by locally proofreading the definitions.

Trying to formally prove something and then failing is a common way people find out they forgot to add an hypothesis.

Another pitfall is defining some object, but messing up the definitions, such that there's actually no object of that kind. This is addressed by using test objects. So suppose you define what a ring is, then you also prove that real numbers and polynomials are examples of the thing you defined.

I'd love to hear a little bit more on what you think the downsides are? (Or a recommendation for a resource to read up on this?)

Add-on story:

I joined binwiederhier for a while in developing Syncany and he invited me for an internship at his current employer.

The experience I gained both in contributing to Syncany and said internship helped me indirectly land the role I'm currently in, and my open source experience in general helped me land a cool engagement where I got to do some innovative open source projects.

Not strictly what you're looking for, but in Lean (functional language/theorem prover), there's some interesting work being done. Using the tool actually shows which suggestions will compile, which certifies correctness to some degree. https://leandojo.org/