No, it can tell you that 42 is the answer to (some lean statement), but not what...

		Someone 5 days ago \| parent \| context \| favorite \| on: “Erdos problem #728 was solved more or less autono... No, it can tell you that 42 is the answer to (some lean statement), but not what question that lean statement encodes.