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/