#jirilebl — Public Fediverse posts

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 #textbook

In 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.

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 #textbook

In 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.