[chongli]

I can't learn math the way you described at all: when things are described by definitions, my eyes glaze over, and nothing is retained. I think the way you are describing filters out a large percentage of people who would enjoy knowing the concepts, leaving only the people whose minds work in that certain way, a fairly small subset of the interested population.

If you told me this in the first year of my math degree I would have included myself in that group. I think you’re right that a lot of people are filtered out by higher math’s focus on definitions and theorems, although I think there’s an argument to be made that many people filter themselves out before really giving themselves the chance to learn it. It took me another year or two to begin to get comfortable working that way. Then at some point it started to click.

I think it’s similar to learning to program. When I’m trying to write a proof, I think of the definitions and theorems as my standard library. I look at the conclusion of the theorem to prove as the result I need to obtain and then think about how to build it using my library.

So for me it’s a linguistic approach but not a natural language one. It’s like a programming language and the proofs are programs. Believe it or not, this isn’t a hand-wavey concept either, it’s a rigorous one [1].

[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[Tainnor]

> When I’m trying to write a proof, I think of the definitions and theorems as my standard library. I look at the conclusion of the theorem to prove as the result I need to obtain and then think about how to build it using my library.

fwiw, this is exactly the thing that you when you're trying to formally prove some theorem in a language like Lean.

[chongli]

I do want to learn theorem proving in Lean just for a hobby at some point. I haven't found a great resource for it though.

[Tainnor]

Have you seen: https://leanprover-community.github.io/mathematics_in_lean/

[chongli]

I hadn’t seen that. Thanks!