Timeline for Learning Math Proof via Proof Assistants
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 31, 2022 at 21:59 | comment | added | Rob Arthan | Kevin's answer is exactly the one I would have given years ago as someone with a mathematical background who got into computer science and then logic and formal specification and proof later. However, I have worked with many colleagues with a computer science background, particularly in functional programming, who have been very successful with using proof assistants to find proofs just by interacting with the machine: they end up with proofs which they don't "completely understand", but that doesn't matter to them. Horses for courses! | |
| Aug 13, 2022 at 18:57 | answer | added | Jim Kingdon | timeline score: 1 | |
| Jul 27, 2022 at 17:47 | vote | accept | quidproquo | ||
| Jul 27, 2022 at 17:10 | comment | added | quidproquo | Thanks @KevinBuzzard, I do not have any formal training in higher mathematics - I will try and get a book like Velleman's and go through that instead. I found the NNG really cool btw, thanks for putting that together! | |
| Jul 27, 2022 at 12:58 | answer | added | zacque | timeline score: 10 | |
| Jul 27, 2022 at 8:32 | comment | added | Kevin Buzzard | So you don't have a math background? My instinct is to recommend a more traditional route. Learning to use a proof assistant is hard enough, learning mathematics at the same time seems to me like it might be too much. It's hard enough getting a proof assistant to accept a proof which you completely understand! | |
| S Jul 27, 2022 at 5:04 | history | suggested | Not An ITP Expert | CC BY-SA 4.0 |
fix tags, some minor copy editing
|
| Jul 27, 2022 at 1:45 | review | Suggested edits | |||
| S Jul 27, 2022 at 5:04 | |||||
| S Jul 26, 2022 at 21:45 | review | First questions | |||
| Jul 26, 2022 at 23:24 | |||||
| S Jul 26, 2022 at 21:45 | history | asked | quidproquo | CC BY-SA 4.0 |