Lean blog post

Stream: new members

[Naman Jaiswal]

just published Lean4: A Comprehensive Guide for Programmers please have a look and give review btw its my first blog https://medium.com/p/lean4-a-comprehensive-guide-for-programmers-f71bf44d46f9?source=social.tw

[Naman Jaiswal]

just published Lean4: A Comprehensive Guide for Programmers please have a look and give review btw its my first blog https://medium.com/p/lean4-a-comprehensive-guide-for-programmers-f71bf44d46f9?source=social.tw

[Michael Rothgang]

Please don't double-post across different threads --- and in particular, not on unrelated topics. This zulip instance is pretty large - with lots of cross-posting, it would become near-impossible to maintain an overview. Thanks.

[Michael Rothgang]

Please don't double-post across different threads --- and in particular, not on unrelated topics. Thanks.

[Michael Rothgang]

(As for the output: this smells LLM-written to me. Somebody should edit wikipedia to mention that mathlib has 200 000 theorems now :-))

[Notification Bot]

3 messages were moved here from #lean4 > Triaging Lean compiler bug by Kevin Buzzard.

[Notification Bot]

2 messages were moved here from #Machine Learning for Theorem Proving > setting up leantool in roo-code by Kevin Buzzard.

[Michael Rothgang]

Also interesting: the quality of the writing seems to deteriorate further down into the text. The text cites itself often; citation numbers are inconsistent for the overall text. (The final LTE blog post gets reused for the continuum hypothesis project, for instance.)

[Michael Rothgang]

Quiz question: which tactic is meant by "Your equation food processor"?

Header

simp