Comment by kurtis_reed
17 hours ago
Accurate formalization is presumably easier than solving the problems, so you can always formalize and check after the solution is generated
17 hours ago
Accurate formalization is presumably easier than solving the problems, so you can always formalize and check after the solution is generated
Typically formalization is actually harder than solving a problem. You almost always solve before formalizing. And it can be surprisingly hard to formalize problems that are easy to solve.
For example, is there a polygon of area 100 that you can fit 99 circles of area 1 inside it, without overlapping? Yes, obviously, it's very easy to prove this informally. Now try formalizing it! You will find it takes a while to formalize a number of fairly obvious geometric statements.
The polygon claim is not at all obvious to me, how do you prove it?