Logic and Proof course ETC and implicit pre requirements

Stream: new members

[Grigoriy Prokhrov]

Greetings! I am going to dig into Logic and Proof course. I finished NNG.

Firstly, what is clear estimated time of completion for this book?

Secondly, what kind of math culture is required if I, for example, decide to study it with my programmer friends? Frankly speaking, it's interesting for me to provide such an experiment with people who actually have no background. Especially, after reading this article.

Thanks!

[Kevin Buzzard]

Which book are you talking about? Is Logic and Proof not complete?

[Mac]

@Kevin Buzzard I think @Grigoriy Prokhrov meant how long does it take (approximately) to read it / complete the exercises.

[Bryan Gin-ge Chen]

You might find @Jeremy Avigad's paper on the Logic and Proof course interesting.

[Grigoriy Prokhrov]

I am sorry for my late answer.

@Kevin Buzzard I've read the article about Lean course at Imperial. Authors mention that students have special course which can be described as "academic writing for human readable math proofs".

@Bryan Gin-ge Chen thank you. Fortunately, I've already read @Jeremy Avigad's article. But basic level of CMU or Imperial student is much higher than average. It's possible to use their knowledge to teach the way of expression on Lean. But I started to feel that in inverse problem of teaching reasoning with computer the Lean may be not enough. If proof is not just a program but mostly a form of communication between people, then it would be that implicit requirement that I mentioned in the opening post.

[Kevin Buzzard]

I agree that right now you cannot just put a mathematics undergraduate in front of Lean and say "go ahead and do maths using this now!"

[Grigoriy Prokhrov]

Ok. It seems like there's no other option to actually know how much time does it take rather than dig into and finish it.

[Bryan Gin-ge Chen]

Do report back after you and your friends have given it a shot! It's always valuable to hear about beginners' experiences.

[Grigoriy Prokhrov]

Thank you! I'll do my best.

[Grigoriy Prokhrov]

So I've started my run in my spare time. It's a nice idea to start this book with logic puzzle. But two things are in my mind. I actually can go through. But this is like a construction kit. A toy for big children with strong motivation. There is definitely a lack of little achievable targets in this journey. An open problem is not an issue for me. Personally, I'm not afraid of working with raw material but this doesn't seem to be a production ready solution. Perhaps this is a reason to invent it?)

As an intern in devops I would like to construct a pretty little theory. Maybe this "theory" will be dumb or trivial, but it will be full-fledged. Even if it would be synonymous with "print x" in other languages. But after every increment I should be ready for release.

There is a difference between filling gaps in NNG theorems and stating&proving own theorems. I see the point of this puzzle. But It would take time to walk through this chapter to personally succeed with exercises. It's look like a waterfall and not like a continuous cycle.

Anyway, I'll finish it.