I started my PhD recently, and in the process I've had to learn Isabelle/HOL, and I gotta say that using it sort of feels like you're unlocking the keys to understanding the universe.

Like, I understand that it's fundamentally still code, and so there are potential bugs in the kernel, but shear versatility and level of automation you get within Isabelle/HOL makes the development and understanding of proof feel like outright magic sometimes. Proof is really hard, and having a powerful tool to mechanically check it has nearly limitless potential.

Someone needs to tell the mathematicians they are allowed to use variable names longer than a single character now.

>> Formalisation of the internal calculus, HF

HF seems 'hereditarily finite'.

I wish someone presents the proof that's 'inlines' the explanation of the terminology used and defines them before using. For something as fundamental as Godel's theorems, this should be worth doing.

I feel like godel incompleteness is a cheap trick that mislead to think there are statements in ZFC that can't be proven except that those proven statement are contrived useless meta-statements.

If Godel's theorem applies to all formal systems. Then in formalizing Godel's theorem, doesn't that make the theorem apply to itself?

So the calculus that formalises the theorem is either inconsistent or there are other true statements about it that can't be proven? Which is it? Can someone with a bigger brain elaborate on how the theorem applies to itself in a language for tiny brained people? No big words please.