#jirilebl — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #jirilebl, aggregated by home.social.
-
Keeping busy with Sudoku, Wordle, Crosswords, and mining textbooks for statements to practice proving in #Metamath ...
Inspired by this video playlist on #RealAnalysis #Math
https://www.youtube.com/playlist?list=PLYPU-RArkLZNwMZ55-y8FZZEeY7zCJX59
Which was created from https://www.jirka.org/ra/ _Basic Analysis:
Introduction to Real Analysis_ by Jiří Lebl. #JiříLebl a #CreativeCommons (4.0) free #math #textbookIn Metamath's compressed format, my proofs of strong induction over the natural numbers took 316 bytes, well-ordering of the natural numbers: 376 bytes, 2ⁿ⁻¹ ≤ n! : 1204 bytes, formula for finite sum of geometric series: 2566 bytes. The last has 147 steps, some of which are reused and some of which depend on up to 8 prior steps and on a truncated library of 30477 statements of syntax, axioms, definitions, and theorems from the wider world of Metamath.