[teiferer]

> Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use:

Here is a other one: hello_world.c versus hello_world.exe (apologies for windows extensions, just for illustration).

One is made by a human for human consumption and extension (though legible by a machine). The source code.

One is made by a machine for a machine. Unreadable by a human. The "binary", though that's a terrible misnomer. (Sure you can disassemble but any nontrivial program is too much to cope with as a whole).

Source vs binary. Both are useful but only one is useful for human consumption.

[dr_dshiv]

Binaries are executed by machines but are not yet understandable by machines. (Now that we live in an era where machines can understand, imperfectly, like us)