How can A freshman learn linear Algebra purely by lean?

Stream: new members

[chenjulang]

Lean4 gives a more easy way to understand math proving procedures.Any Advise on learning Algebra purely by lean?

[Riccardo Brasca]

It is usually a bad idea to learn math at the same time of formalizing it. Something more reasonable is to study linear algebra in the usual way and from time to time trying to formalize certain results.

[Riccardo Brasca]

But I strongly suggest to ask for some help here on what to formalize, since often writing the statement can be a little tricky.

[chenjulang]

maybe formalizing is the best way to learn , in long term? Because it is easily traceable, and mostly , it is true（I think we sometimes pretend to understand the proof steps in the math books and then skip them.Lean never let you skip）

[Riccardo Brasca]

The problem is that you have to fight with the math and with the formalization at the same time

[Riccardo Brasca]

and mathlib is not at all written with pedagogical purposes in mind (for example there are no vector spaces, but only modules, that are a generalization, so you will be quickly confused not finding what you are learning)

[Riccardo Brasca]

I am not saying you should avoid using Lean at all, but you can use it sometimes. But I really suggest that most of the learning should be done in the usual way.

[chenjulang]

Riccardo Brasca said:

and mathlib is not at all written with pedagogical purposes in mind (for example there no vector spaces, but only modules, that are a generalization, so you will be quickly confused not finding what you are learning)

You are right, the modules...

[Bulhwi Cha]

Riccardo Brasca said:

It is usually a bad idea to learn math at the same time of formalizing it.

I plan to learn linear and abstract algebra next year by reading relevant Mathlib files and some textbooks. I'll need to select exercises to solve in Lean.