Email Gateway (Aug 22 2022 at 18:00): Email Gateway (Aug 22 2022 at 18:00):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
I learned Isabelle, Coq and UniMath without professor, just from the
manuals and I did not studied computer science neither (just pure
mathematics).
The following points are key advices for an hypothetical beginner in
Isabelle according to my personal experience (the learning process varies
from person to person):
(1) Look at easy examples and try to prove similar theorems by yourself.
You could look at my implementations (I regular update my repertory), which
are nice from a pedagogical point of view:
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory
(2) Read the manual only when you need it and do not read it as a novel:
practice in Isabelle is more important than theory.
(3) Do not look at the proof state, just focus on your Isar code.
(4) Break your main theorem into several lemmas (having lower complexity
than your original theorem) and put sorry in each one. Then, prove your
theorem assuming that the lemmas are true. After that, repeat the same
process to each one of your lemmas.
(5) Drink as much coffee as you medical doctor allows you. Sleep 20 minutes
after drinking the coffee and before beginning to write in Isabelle. This
will amplify your focus (there are scientific evidence of coffee naps):
https://blog.bulletproof.com/coffee-naps-bulletproof-power-nap/
(6) Do one activity at time (the human brain is not multitask). Do lo
listen music while you are coding.
Well, I hope that these advices will help people. Isabelle as easy learn as
possible, what is hard is mathematics itself, and of course, its formal
verification in Isabelle.
Kind Regards,
Jose M.
Last updated: Apr 18 2024 at 12:27 UTC