Hacker News Reader

Accurate formalization is presumably easier than solving the problems, so you can always formalize and check after the solution is generated

View on HN

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?

Draw 99 circles in a row, then draw a separate polygon around each one with only a teeny amount of excess area, then connect those polygons with teeny little connectors to make it a single polygon. When I say "teeny", you can make those arbitrarily small, so you can certainly fit them under 1 total area.

Okay, it's maybe not "obvious" in a regular human sense, but in a graduate math class you could claim this was "obvious". It would be pretty clear if I were drawing a diagram on a whiteboard. I would definitely take less time proving this to a human, than formalizing it.

Reply on news.ycombinator.com