Key Themes from the Discussion
| Theme | Summary (with supporting quote) |
|---|---|
| 1. Critical evaluation of “standard” choices | “Every time you go off the beaten path, you're locking yourself into less documentation, more bugs … If you've got 20+ choices to make, picking the standard option is the right choice on average, so you can just do it and move on.” – sdenton4 |
| 2. Lean’s pragmatic blend of classical and constructive logic | “The creators are very pragmatic, which is why they encode classical logic in Lean types, with only a bit of intuitionistic logic.” – smj-edison |
| 3. Barriers to widespread adoption of proof assistants | “I think this is one reason most mathematicians don't see a need for formal proof assistants, since from their perspective it's one very small part of math, and not the interesting one.” – jsmorph |