announcement - beginner-friendly content

Stream: new members

[rzeta0]

So I've started to blog and create videos as I learn Lean for the purpose of writing simple maths proofs.

I'm no expert in maths, nor coding, but I guess I do have some insight into the barriers and challenges newcomers face .. and for that reason I'm sharing what I'm doing.

I welcome questions and ideas from beginners for topics or specific confusions we can collectively resolve together.

I realise a lot of the community here are deeply experienced highly advanced experts - but this content is aimed at people who are intimidated by all that :)

:movie_camera: youtube
https://www.youtube.com/@LeanFirstSteps/videos

:books: blog
https://leanfirststeps.blogspot.com/p/contents.html

👩🏻‍💻 github
https://github.com/rzeta0/Lean-First-Steps/

[Shreyas Srinivas]

For the blog, I believe if you use verso you can get in-place proof state

[Eric Wieser]

Yes, if you're interesting in writing about Lean, it would be great to have more people trying out (and becoming experts in!) Verso

[rzeta0]

I can't do Verso as it requires me to have a build system, as far as I can tell.

I just want to be able to "write content" with minimal coding (html).

Let me know if II've misunderstood Verso. Is it something I can embed as HTML in blogger?

[Shreyas Srinivas]

I am not an expert on verso, but I understand that it can accept markdown which in turn allows HTML to be embedded in it.

[Eric Wieser]

I can't do Verso as it requires me to have a build system, as far as I can tell.

Yes, this is the main friction. Ideally there'd be a template github repo you could clone that does all the build and deployment stuff for you, so that you can focus on content

[Shreyas Srinivas]

I am not sure this build system requirement is a bad thing since all static blog generators require some sort of a build system and folder setup.

[rzeta0]

some of us old and tired people don't have the energy or capacity to have static blog generators - we just use a browser to log in, type, and hit publish .. and occasionally - with a sigh so deep and profound it actually knocks Pluto's orbit off - we "edit html" to do <code>

[Jose A. Alonso]

rzeta0 ha dicho:

So I've started to blog and create videos as I learn Lean for the purpose of writing simple maths proofs.

There is a blog ( https://jaalonso.github.io/calculemus ) in which an exercise is proposed daily and its solutions are published in Lean4 and Isabelle/HOL