I know nothing about theorem provers. Is the idea that you can prove a large number of simpler statements that build on each other until it all implies the top level theorem you're proving (like how IRL math works)? That way you don't have to understand the gargantuan computer program all at once?
It just seems like it would be as hard to verify the accuracy of the code written to prove a complex theorem like FLT as a manuscript written in English. But if you can rely on smaller statements that build on each other, it would make more sense.
The way it works is that if you trust the theorem prover to be bug free, then you only have to verify that the theorem was correctly stated in the program. The proof itself becomes irrelevant and there is no need to verify it.
I use a program called earlyoom. It will monitor RAM and if you cross a level of utilization (default 95%?) it will kill the worst offenders before the system becomes unresponsive. You can layer on sophistication like protecting certain programs or preferring killing others. I find it invaluable when I am doing data science work and do something stupid which explodes in memory. Annoying that something was killed, but usually better than hosing the entire system -if it crossed 95% it was almost certainly going to hit 100%.
For my purposes it works perfectly - only the Python process will be killed, my IDE or notebook will survive.