Any project that starts from an undergraduate perspect?

Stream: new members

[chenjulang]

Is there any project that starts from an undergraduate perspective and then proves the theorem step by step?
Because for those who are new to a certain field, if a low-point definition can be provided, they will be more motivated to learn.

[Marcus Rossel]

Which field of study are you interested in? As an example of an undergrad project, this repo formalizes and proves properties of a certain model of computation from first principles: https://reservoir.lean-lang.org/@lf-lang/reactor_model (related paper: https://cfaed.tu-dresden.de/files/Images/people/chair-cc/publications/2310_Rossel_VSSTE.pdf)
But that's a very computer sciency (and rather niche) topic.

[chenjulang]

any fields would do.

[chenjulang]

I want to see projects that is independent from the mathlib4. I mean , definitions should have more easy or straightforward version. That should lead to a simpler proof somehow, right? And saves a lot of time for new users.Just take what they need and form the maths. Simple is beauty , Agree?

[Patrick Massot]

No, abstract proofs are very often simpler. And this is even more true in a proof assistant.

[Kalle Kytölä]

Regarding simplicity of proofs, Patrick's comment is absolutely correct (although it is not uncommon that people start by somehow expecting the opposite).

But simplicity is not the same as being easily approachable from an undergraduate background. So the original question on projects distinct from mathlib for pedagogical purposes is a very meaningful one.

I would not require such projects to be independent of Mathlib, though. There is room for various formats, of course, but I believe a fruitful approach would be to build on Mathlib and thus get for free all of the things that are assumed common knowledge but never actually addressed in undergraduate courses. (A simple example could be doing calculus before defining real numbers --- it would certainly be convenient to take Mathlib's real numbers as well as a few other things.)

In any case I don't have a great answer about existing projects of this type, but I think we would all welcome such resources.

(Maybe worth mentioning here is the course/textbook The Mechanics of Proof, which builds on Mathlib but deliberately offers the user a more undergraduate-appropriate interface.)

[Kalle Kytölä]

(Should we have a Zulip linkifier to The Mechanics of Proof, btw?)

[Kalle Kytölä]

Of course many components of #mil are deliberately pedagogical, too, but it seems much more geared towards introducing the reader to Mathlib proper.

[chenjulang]

Or can I ask another question? Any projects translate a textbook into lean step by step ? Like this one : https://github.com/martincmartin/linear_algebra_done_right