Banach-Tarski complete

Stream: general

[Arthur Tilley]

Hi all,

I'm happy to announce that the Banach-Tarski project is now, sorry-free, linted, and has a base level of comments/documentation.

The proofs in this project are still certainly pretty verbose compared to what I see in Mathlib, so I'll be coming back to this project in the future to tighten things up as I learn more about Lean.

If anyone has and suggestions (ie. about what sections could use more comments / explanation) please do reach out.

Thank so much to all the folks that took time to answer questions and offer suggestions. (Also a special thanks to @Tanner Duve to being available to answer my questions back when I was working through the natural numbers game.)

sincerely,
Arthur

[Tanner Duve]

Nice work man

[Johan Commelin]

Does that mean that you can now cut the project into 5 pieces and assemble them again into two identical copies of the project?