Open sm4sa opened 1 year ago
"The second part of the class will focus on how to formalized abstract mathematical structures in Lean, and how we might such capabilities to these advances in formalizing mathematics to help meet the need for statically type checked specifications in the abstract language of the domain, with corresponding parametric representations carried along for computational possibly and oher purposes."
"formalized" should be changed to "formalize" In the part "and how we might such capabilities to these ...", I believe might is a typo and should be changed for clarity. "other" should be changed to "other"
We will mainly use Lean 3, nothwithstaning that Lean 4 is garnering real attention and effort.
The typo "nothwithstaning" should be changed to "notwithstanding".