this is a lean 4 fan account now

maybe not a fan of starting out with `calc` (its syntax is convenient but weird imo), however the intro is golden [Introductory Proof with Lean 4...]( )

finished my first “serious” formalization (i.e. it’s an actual theorem, not a toy example). this is based on an example from the book i’m reading (Mathematics in Lean) but i rewrote the code on my own from scratch to better understand the proof. it was fun! (and took me the whole week) [Formalization of Schröder–Bern...](

Gist

Formalization of Schröder–Bernstein theorem in Lean, based on an exercise from Mathematics in Lean

Formalization of Schröder–Bernstein theorem in Lean, based on an exercise from Mathematics in Lean - schroeder_bernstein.lean

)

fwiw i’ve seen bsky app do this before too, wonder if some RN issue? only happened on testflight builds for me tho RE:

Bluesky Social

_ (@kasey.cafe)

���� ��� ���� �

spent most of the day trying to understand the proof of Cantor-Schroeder-Bernstein and i think i almost get it, it’s kind of like stitching?

writing proofs in lean feels just like coding except your entire program is a noop and your only job is to make it typecheck

poor craftsman blames his tools. good craftsman blames his ancestors

the (relatively) new "report convo -> spam -> block & delete" workflow is so satisfying

obsidian is nice. glad roam didn’t just die with the stale product

would be nice if @Bluesky coalesced “trending” feeds on the same topic from different periods when they were trending https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreigv6cyhbtn7itqyawn5rg37zhue6v6lmjtokvc3dsjbnt5r5gi2jq