News for hackers. Stuff that matters.

A comment on Interactive Linear Algebra Dan Margalit, Joseph Rabinoff. Parent comment

Re:Interactive Linear Algebra Dan Margalit, Joseph Rabinoff by 0cf8612b2e1e on Sunday September 01, 2024 @09:47PM (#41421904)
Something that drives me up the wall is just how sloppy math notation can be. Supposedly this pure discipline, but many authors use custom conventions all over the place, shorthand, skip steps, etc.

Give me some math code, where the end result has to compile. No sneaky tricks allowed.

[ Parent | on HN ]
Re:Interactive Linear Algebra Dan Margalit, Joseph Rabinoff by lanstin on Sunday September 01, 2024 @11:09PM (#41422299)
You want mathlib, the lean library of established results: https://github.com/leanprover-community/mathlib4

They skip steps in writing because they can generally do them and it obscures the flow of the argument to have every thing spelled out.

There is also a book on mechanics by the authors of SICP: https://mitpress.mit.edu/9780262028967/structure-and-interpr...

[ Parent | on HN ]
Re:Interactive Linear Algebra Dan Margalit, Joseph Rabinoff by thaumasiotes on Monday September 02, 2024 @01:09AM (#41422759)
> They skip steps in writing because they can generally do them and it obscures the flow of the argument to have every thing spelled out.

They do that in lean too; that's the idea of simp.

[ Parent | on HN ]
Re:Interactive Linear Algebra Dan Margalit, Joseph Rabinoff by lupire on Monday September 02, 2024 @11:44AM (#41426407)
Lean doesn't have expressiveness notation. It's like Perl line noise.
[ Parent | on HN ]