That basically implies the second option: some mathematical truths are beyond the grasp of humans. Which I suppose isn't too weird, it's entirely conceivable th

That basically implies the second option: some mathematical truths are beyond the grasp of humans. Which I suppose isn't too weird, it's entirely conceivable that for some theorems the shortest possible statement of them simply can't be understood in a lifetime, or ever. Which to me makes more sense at least than the first option, which seems to argue that human minds cannot be mechanized because humans are capable of proving mathematical truths and machines have mathematical truths they cannot prove.