> 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.