4 ms·
Yes, in the sense that "math is programming paper instead of computers", being better at one translates to being better at the other. This intuition can even b
by wisnesky 3y ago
Yes, in the sense that "math is programming paper instead of computers", being better at one translates to being better at the other. This intuition can even be made precise via the "Curry-Howard isomorphism", upon which "proof assistants" such as Coq are built.
- westurner 3y agoLean mathlib was originally a type checker proof assistant, but now leanprover-community is implementing like all math as proofs in Lean in the mathlib project. Lean (proof assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant) "Lean mathlib overview": https://leanprover-community.github.io/mathlib-overview.html https://leanprover-community.github.io/mathlib-overview.html "Where to start learning Lean": https://github.com/leanprover-community/mathlib/wiki/Where-to-start-learning-Lean https://github.com/leanprover-community/mathlib/wiki/Where-t... leanprover-community/mathlib: https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib