Thought of the day: I think mathematical-Platonist "discovery" is what some form of mathematical-constructivist "computation", most likely a stochastic search problem, feels like from the inside. After all, our intellectual faculties were tuned by evolution to locate physically real objects in physically real spaces, so repurposing the same cognitive machinery for "locating" an object for an existence proof would feel like locating an object in a space, even if the "space" and "object" are just mental models and never really existed in any physical sense.