> I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods.
> Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what to use them for and how.
How is any of that different from what we had in math before Lean?
It is more software ish. You don't just have a citation to earlier results, you can import the library. And you don't have to trust collaborators as much, the proof engine validates. And you can use github to coordinate large projects with incremental but public progress.
> Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what to use them for and how.
How is any of that different from what we had in math before Lean?