[fnrslvr]

> Even in the much cleaner world of mathematics, basically all interesting work is done within the realm of formally provable statements.

More-or-less this. I'm going to take this as an opportunity to drop one of my favourite quotes, because I can't help it:

"The view that machines cannot give rise to surprises is due, I believe, to a fallacy to which philosophers and mathematicians are particularly subject. This is the assumption that as soon as a fact is presented to a mind all consequences of that fact spring into the mind simultaneously with it. It is a very useful assumption under many circumstances, but one too easily forgets that it is false. A natural consequence of doing so is that one then assumes that there is no virtue in the mere working out of consequences from data and general principles."

-- Alan Turing, Computing Machinery and Intelligence

[wolfram74]

I like to think about the 4th quadrant of the known-unknown punnet square: the unknown Knowns, things definitively implied by what you already know but haven't realized yet. Latent knowledge like that is often fun to play with, especially with students, getting them to realize they understand more than they think they do.