Slashdot Mirror

Here is the relevant law:

The right of the people to be secure in their persons, houses, papers, and effects, against unreasonable searches and seizures, shall not be violated, and no Warrants shall issue, but upon probable cause, supported by Oath or affirmation, and particularly describing the place to be searched, and the persons or things to be seized.

This is the Superior Court of DC, so I think this is actually the relevant law on search warrants:
https://beta.code.dccouncil.us/dc/council/code/sections/48-921.02.html

The Constitution doesn't exactly provide a lot of details, so one normally looks at the actual laws on the subject. To re-derive the constitutional contours of search warrants from constitutional principles every time would be sort of like trying to do this every time you want to add 2+2. In short, no, it doesn't work that way.

It's normal for demands to be overly broad. They ask for whatever they might plausibly get, because sometimes the judge agrees with them and they won't get anything they don't request. This is how an adversarial justice system works. There are other models, for example, inquisitional systems, in use in other countries.

Note that I am not arguing with you about this being non-public information. You were right to correct the other poster about that. And you were right that it is, in fact, completely obvious from the fact that they issued a search warrant. The judge realized there were real concerns here, so they narrowed the scope of what was asked and are allowing the police to search it first, then unmask people later if they have probable cause to believe they were participants in a crime.

In short, it's a detailed and perfectly sensible decision that appears to be quite fair to both sides.

Depends on what set of axioms you pick as your base set, and some common choices don't have have that as an axiom because it is (easily) provable from a more basic set of axioms. For example, using something similar to Tarski's set of predicate calculus axioms requires something like 9 steps if being explicit.

> will continue to unless you can provide a proof.
Assuming you're not lying:

http://polymathematics.typepad.com/polymath/2006/06/no_im_sorry_it_.html
https://en.wikipedia.org/wiki/0.999
http://us.metamath.org/mpegif/0.999....html

It's worse than that. Not only is math equivalent to software, but people have written the programs for ZFC (if you don't know what that is, just replace ZFC with "all the math you know and then some"). You can play with that program over on Metamath if you're so inclined.

I thought you might have taken the time to look things up, but apparently not. Let's recap then; Euclid proved that there are infinitely many primes in approx. 300 BC. The proof is very straightforward and has been repeated many times. See here for a canonical example. But wait, there's more. Bored mathematicians have found other proofs, usually perverse ones for amusement value. See, for example Goldbach's proof, or Furstenberg's topological proof.

Perhaps your going to say that those are just a touch hand-wavy and not "derived directly from mathematical laws". That would be a mistake, but we can cover that too: here is a proof that is conveniently completely machine verifiable and traceable back to formal axioms -- specifically first order predicate calculus and Zermelo Frankel set theory (we don't even need the axiom of choice!).

There are infinitely many primes. But don't trust me -- work through the metamath proof in all the gory details if you really still don't believe.

And what is this about programming having a strong mathematical foundation?? It's a list of things to do, about the only math needed is some understanding of Boolean algebra, which should only take an hour to learn.

Formal mathematics is ultimately done with sets of symbols and rules for building formulas from axiomatic sequences of symbols. In essence it's string processing with a few special rules about the symbols that represent variables. Getting to arithmetic from that point is a long road, but once you realize that mathematics is just formal rules it's no surprise that a subset of formal mathematics is the context free languages used for programming. This is important when you need to prove things about classes of programs or transform programs from one programming language into another or prove that all programming languages can compute the same things as a Universal Turing Machine.

Look at metamath for an interactive bottom-up approach to constructing mathematics and I think you'll see the similarity to programming.

Or is it the program that interpreted the chess game into music? That is, would a bunch of random numbers being fed into the program produce just as good of a sound? Sometimes I wonder about these things.

This is an interesting question, although I don't know the answer for this chess music.

There is another project that plays the nesting level of logic proof "trees" as notes, mapped more or less directly without interpretation, with somewhat interesting results. From http://us.metamath.org/mpegif/mmmusic.html

Unlike a proof's tree structure, which is inherently suggestive of a musical score, the digits of pi have no obvious pattern. To make it interesting, a human composer will often add a non-mathematical creative element such as an underlying beat with pre-selected chords and instrumentation.

Here's the amicus brief written by the IEEE-USA president Professor Lee A. Hollaar. I direct your attention to footnote #28, which reads in relevant part:

It is unfortunate for purposes here that the early developers of programming language made their calculation-and-assignment statements look like mathematical equations so that they would seem familiar to scientists and engineers. But the common programming statement I = I + 1, which increments the value stored at location I, is essentially nonsense as a mathematical equation. Similarly, a computer program is a series of calculation-and-assignment statements that are processed sequentially, not a set of simultaneous mathematical equations that are solved for their variables.

(Freshly transcribed from the PDF; feel free to check for typos.)

Yes, I wrote it wrong when I said 1+1 instead of I+1 before. But however you write it, we're dealing with the successor function (either in general, or the successor of 1). It's related to the second Peano axiom as a function that helps us define the natural numbers (and thereby, the integers, rationals, reals, etc.).

But you knew that already, right? That's why you just threw up a [citation needed] rather than actually respond?

I suppose you must be two of a kind, with him calling the correspondence between programs and mathematics "cosmetic" rather than actually addressing it. To be fair, I suppose that proving the Curry Howard correspondence wrong would be a bit more of a challenge.

I mean, how do you disprove it or consider it "cosmetic" when the fine folks at MetaMath are writing out the foundations of mathematics as a computer program?

If you simulate a physical process on a computer, say, the sun going nova, you can look out the window and the sun will still be there (it hasn't actually gone nova). If you "simulate" a mathematical process on a computer, you end up with the same result as if you'd done it by hand (assuming you don't screw up).

You don't seem to understand the Curry-Howard correspondence. Software is math in a fundamental way that does not apply to physics, chemistry, etc. Software sets up a calculation. It *is* math, it doesn't just use math. It doesn't merely describe software, it implements it. Unless you're going to claim that all of reality is running on a computer somewhere, or that Earth itself is a giant calculator for mice...

A computer is nothing more than an automatic mathematician. If we call the work of mathematicians like me "math" why is that different from what we call the same work done by a machine ("software")? Check out the work of these guys sometime and tell me exactly where the imaginary line goes. Or please give us an example of a "non-mathematical" program. We'll be happy to point out that it is, in fact, a big number and show you the connection to Godel.

If your goal is to permit software patents, you would do better to remove the blanket exemption of "math" (or else, limit it to mathematics not done by machine), rather than trying to pretend that math done by machines is no longer math.

Oh, by "infinite music" I thought they meant algorithmically generated music. Like this piece of music from the Metamath Music Page.

A golden age for that? Were there breakthroughs in artificial neural networks I hadn't heard of? Or have musical expectations fallen just that low?

I do wonder what would happen if you took the output from a random number generator to make a valid MP3 file and then played back that MP3 through an Autotuner.

Oh, by "infinite music" I thought they meant algorithmically generated music. Like this piece of music from the Metamath Music Page.

A golden age for that? Were there breakthroughs in artificial neural networks I hadn't heard of? Or have musical expectations fallen just that low?

I do wonder what would happen if you took the output from a random number generator to make a valid MP3 file and then played back that MP3 through an Autotuner.

> All inventions can be described by math - that is nothing unique to software.

No. We can model them, but not accurately. Heisenburg uncertainty alone keeps our representation from being true, not to mention the unfathomable number of numbers you need to actually represent something. Not to mention that we don't actually know all the laws of physics, or there'd be no question about which interpretation of QM is correct.

Anyhow, the claim isn't that software can be described by math. The claim is that software is math. Or to be more specific, any software can be converted into a mathematical statement (this is hard, but thanks to Curry-Howard, it is possible). Further, any math can be converted to software (see this project, which is converting the main axioms of math into software).

Because we can transform one into the other, we call them equivalent. So patenting software patents the equivalent math. There exists math which you can no longer do without a computer (e.g. computer proofs of the four-coloring theorem). So badly written patents can exclude the use of math (unless they are invalidated on precisely those grounds).

> Software is just a step-by-step instruction list. It's is no more a form of math than is a cookbook.

You might want to look up Curry-Howard correspondence someday.

Not only is software math, there's an equivalence theorem relating the two. If that were not the case, the people over at MetaMath wouldn't be able to get very far.

In other words, that statement isn't just wrong, it's provably wrong and you'll have to prove the Curry-Howard correspondence wrong before you can claim otherwise. One of the weird properties of a correspondence is that you can turn software back into math.

I know that people think that math is all arithmetic and integrals or something, but that's just not true.

> But is a program that stores and displays recipes, math?

Yes. The recipes all correspond to binary numbers (as does any other data). The search function in it is a mathematical function that maps queries to results. The UI maps the binary numbers from sensor devices to the numbers that represent the on-screen output.

Like I said, you don't know what math is, you only think you do. Numbers are no different than any other precise form of information. You're trying to ignore a mathematical proof by relying on your incorrect understanding of what math is.

If you really want to debate something, you'd have to say that perhaps mathematics shouldn't automatically be unpatentable by statute. Frankly, mathematics being unpatentable is one of the few parts of patent law I completely agree with. I just wish they'd realize that math IS software and software is math.

There's no clear distinction between the two. For any stupid "non-mathematical" program you come up with, we can translate it back into pure math.

I wasn't logged in before, GP anon was me. Anyhow, the period was the end of the sentence, not some attempt to make it into a float/string/boolean/whatever and I certainly didn't use the Python operators. It's supposed to be the same token (1) on both sides. But that's why we use formal languages that are picky about syntax and which can be checked automatically to avoid people finding weird ambiguities to question.

The theorem I was mentioning above is called Curry-Howard-Lambek correspondence (it took me a while to find all the links):

The Curry-Howard-Lambek correspondance is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and vice versa).

(Wiki links added because most people are too lazy to Google the terms they don't understand. Especially if they don't realize that they don't actually understand them.)

So even if you find some crazy language where they define != to be an equality operator or something equally unusual, software is still equivalent to math. Metamath wouldn't be possible otherwise. And as you can see, they're doing just fine.

My degree is in mathematics. There's no such thing as non-mathematical software. There is mathematical proof of this. There's a nice equivalence theorem for the two, and the website linked shows the results of that equivalence.

I repeat: there's no such thing as "non-mathematical" software, because it is equivalent to math. The only people who think otherwise don't know what math is. It's like trying to claim that 1 != 1. And yes, people really do claim utter nonsense like that sometimes, especially those who don't understand the fact that infinite sequences like 0.99999[repeating] don't have a last digit by virtue of being infinitely long (if an infinite list had a last element, it would be a contradiction in terms, because part of the definition of infinite is that for every element x, there is a successor of x).

One might as well claim that pi is exactly 3.

http://us.metamath.org/latex/realref.sty

What this does is have \ref's jump to the actual point of the anchor in the PDF document instead of just the top of the page, making the PDF (IMO) far nicer to use. (It's been a few years - if hyperref now does this, someone kindly correct me.)

To use it, \usepackage{hyperref} followed by \usepackage{realref}. I've used it many times and it has worked perfectly for me.

Metamath is doing pretty much this, for ZFC. It's an interesting project. All 193 propositional calculus theorems from the Principia Mathematica have been proven. >8000 theorems total proven.

Metamath is doing pretty much this, for ZFC. It's an interesting project. All 193 propositional calculus theorems from the Principia Mathematica have been proven. >8000 theorems total proven.

There's a website called Metamath which does a lot of what the article is talking about. It starts from the ZFC axioms and works its way up to thousands of elementary theorems, all proved completely formally. Pretty cool, if you're in to that sort of thing.

I can give a concrete answer. Browse metamath.org, a similar project in which machine verified proofs are collected. Look at the vast amount of work required to prove even the most trivial things. ... Converting real world mathematics into machine readable form is a vast endeavor. It's also something that doesn't interest mathematicians, so the collection of machine verifiable proofs will lag *centuries* behind the state of the art.

This is probably correct if you're talking about minimalistic systems like Metamath or Russell & Whitehead's Principia.

What such projects are attempting is like trying to build a concrete building by gluing grains of sand together by hand, or writing a complete Linux distro in assembly code. The result does not prove that the ideas of building from concrete or writing software are a failure, only that you need the right tools to do that.

There is an interesting note by Freek Wiedijk which estimates the effort required for a "standard library" of formalized mathematics as about 140 man-years.

This assumes a "de Bruijn factor" of about 4 (i.e. one page of informal mathematics translates into four pages of formalized language) and a cost of ~2 man-days per page of formal mathematics. Both of these will undoubtedly be improved by further research.

Perhaps we shouldn't worry about this, though. To many people, doing formalized mathematics is as fun as writing computer code; why should we worry that the supply of that fun is near-limitless?

This is indeed what one would expect. For that reason I find matemath far more interesting. Isabelle already has been use for some time. According to the wikipedia entry: "It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness."

Wouldn't it be better to get something like an ajax version of http://metamath.org/ up?

I can give a concrete answer. Browse metamath.org, a similar project in which machine verified proofs are collected. Look at the vast amount of work required to prove even the most trivial things. For example check out 2+2=4. Make sure you drill down into the proofs of the theorems used, not just the top level. Converting real world mathematics into machine readable form is a vast endeavor. It's also something that doesn't interest mathematicians, so the collection of machine verifiable proofs will lag *centuries* behind the state of the art.

I can give a concrete answer. Browse metamath.org, a similar project in which machine verified proofs are collected. Look at the vast amount of work required to prove even the most trivial things. For example check out 2+2=4. Make sure you drill down into the proofs of the theorems used, not just the top level. Converting real world mathematics into machine readable form is a vast endeavor. It's also something that doesn't interest mathematicians, so the collection of machine verifiable proofs will lag *centuries* behind the state of the art.

A proof is different then from invention or process. A proof would verify that a compression would work, perhaps it could explain the outer bounds of limits to the proof. But it doesn't nessarly give the process.

A formal proof that an algorithm is correct is enough information to implement the algorithm, since each step of the algorithm must exist as part of the proof. There is no way to formally verify that an algorithm works without showing that each of its operations has a well defined action, and that the result of all the actions yields the correct output.

There are non-constructive proofs of theorems, but the proof itself can ultimately be treated as an algorithm for applying the axioms of a formal system in order to generate the proof. The problem remains that if it is possible to patent software algorithms, then it must be possible to patent mathematical proofs. See metamath for a good example of why and how it can work. Mathematical proofs can be reduced to a formal language which describes an algorithm for applying axioms to a sequence of well formed formulas.

http://us.metamath.org/mpegif/projlem7.html

On my (older) 1GHz computer, this takes 65 sec in Firefox 2, but only 16 sec in IE. (The whole metamath site is annoying in Firefox because of its slowness.)

One potential weakness with metamath is that definitions are introduced without formal proof. This is acknowledged by the developers, and the definitions are generally straightforward enough that the results can be judged as correct. For instance, see df-2, which if ever used to represent the mathematical concept of 2 (e.g. by a parser seeing the digit "2" and replacing it with df-2), depends entirely upon the axiomatic definition of df-2 as (1 + 1). It is possible for someone to define df-2 as ((1 + 1) + 1), and a proof relying only on df-2 (e.g. not reducing all terms to the ZFC axioms) could actually prove a false statement given the new definition of df-2 (but it's old interpretation as the number 2). The problem arises when definitions are substituted for actual constructions of the basic axioms of the formal system without proof that the definitions themselves are sound.

Apparently the Ghilbert project does produce formal proofs of definitions and can import metamath proofs, but I have not looked at it much.

See mmset appendix 4 for references.

One potential weakness with metamath is that definitions are introduced without formal proof. This is acknowledged by the developers, and the definitions are generally straightforward enough that the results can be judged as correct. For instance, see df-2, which if ever used to represent the mathematical concept of 2 (e.g. by a parser seeing the digit "2" and replacing it with df-2), depends entirely upon the axiomatic definition of df-2 as (1 + 1). It is possible for someone to define df-2 as ((1 + 1) + 1), and a proof relying only on df-2 (e.g. not reducing all terms to the ZFC axioms) could actually prove a false statement given the new definition of df-2 (but it's old interpretation as the number 2). The problem arises when definitions are substituted for actual constructions of the basic axioms of the formal system without proof that the definitions themselves are sound.

Apparently the Ghilbert project does produce formal proofs of definitions and can import metamath proofs, but I have not looked at it much.

See mmset appendix 4 for references.

A problem with Metamath is that it is very labor-intensive to develop proofs.

It may be argued that computers are not really an appropriate tool when truly "correct" mathematics must be relied upon. My response to that is that as problems of interest become ever more complex, limitations both of the human mind and the human life span will ultimately limit the problems we can solve unaided. The task for us now is to create a system we CAN trust to solve problems correctly, because someday we will have to trust it to solve problems we cannot handle.

There is a mathematical proof verification language, Metamath, whose rigor and/or correctness (meaning freedom from bugs) are probably near the top, if only because (1) the proof language is trivially simple and (2) as a result half a dozen independently written proof verifiers have been coded, in C, Haskell, Python (300 lines of code), Java, Lisp, and Lua, so the likelihood they all have the same bug is pretty small. It stands in contrast to some other proof verifiers or theorem provers that embed complex internal algorithms and tend to be very large programs that would be hard to formally verify for correctness - and in some cases are closed source (like Mizar, which BTW probably has the largest body of mathematical knowledge developed for it).

A problem with Metamath is that it is very labor-intensive to develop proofs. The proof of 2 + 2 = 4 has 23,000 steps from ZF set theory axioms, and the computation of cosine of 2 to one decimal place has some 75,000 steps that take several seconds for the verifier to verify. All of these steps were entered by hand (although once a collection of theorems are developed they can be reused, so proofs become easier as a body of knowledge is developed). All of these steps are absolutely, rigorously correct - assuming that at least one of the independent verifiers has no bugs. Unlike a 75,000 line computer program, there is no such thing a a bug in the proof - a proof is either right or wrong (i.e. not a proof).

It may be argued that computers are not really an appropriate tool when truly "correct" mathematics must be relied upon. My response to that is that as problems of interest become ever more complex, limitations both of the human mind and the human life span will ultimately limit the problems we can solve unaided. The task for us now is to create a system we CAN trust to solve problems correctly, because someday we will have to trust it to solve problems we cannot handle.

There is a mathematical proof verification language, Metamath, whose rigor and/or correctness (meaning freedom from bugs) are probably near the top, if only because (1) the proof language is trivially simple and (2) as a result half a dozen independently written proof verifiers have been coded, in C, Haskell, Python (300 lines of code), Java, Lisp, and Lua, so the likelihood they all have the same bug is pretty small. It stands in contrast to some other proof verifiers or theorem provers that embed complex internal algorithms and tend to be very large programs that would be hard to formally verify for correctness - and in some cases are closed source (like Mizar, which BTW probably has the largest body of mathematical knowledge developed for it).

A problem with Metamath is that it is very labor-intensive to develop proofs. The proof of 2 + 2 = 4 has 23,000 steps from ZF set theory axioms, and the computation of cosine of 2 to one decimal place has some 75,000 steps that take several seconds for the verifier to verify. All of these steps were entered by hand (although once a collection of theorems are developed they can be reused, so proofs become easier as a body of knowledge is developed). All of these steps are absolutely, rigorously correct - assuming that at least one of the independent verifiers has no bugs. Unlike a 75,000 line computer program, there is no such thing a a bug in the proof - a proof is either right or wrong (i.e. not a proof).

http://metamath.org/ has been around for 15 years or so; it has a very nice text-based proof expression, a huge library of existing proofs and a graphical visualization tool

Even better, check out the The Comprehensive LaTeX Symbol List (PDF file). For a quick and dirty overview of what kinds of symbols aren't in Times New Roman, a large scientific/mathematical subset of these have been converted to screen bitmaps: GIF and PNG Images for Math Symbols.

On Windows, the GIF image versions of the Metamath pages render slower on Firefox than on Internet Explorer. The Firefox extension IE Tab solves this problem by using the IE rendering engine under Firefox. For example, the web page http://us.metamath.org/mpegif/projlem7.html (870K), when loaded locally (to eliminate the network speed) on a 1.2GHz Celeron, took 65 seconds to render on Firefox but only 12 seconds after right-clicking to reload it with IE Tab. However, IE Tab can't be used for the Unicode version, since (like IE) it renders the fonts incorrectly.

-- Norm Megill

On Windows, the GIF image versions of the Metamath pages render slower on Firefox than on Internet Explorer. The Firefox extension IE Tab solves this problem by using the IE rendering engine under Firefox. For example, the web page http://us.metamath.org/mpegif/projlem7.html (870K), when loaded locally (to eliminate the network speed) on a 1.2GHz Celeron, took 65 seconds to render on Firefox but only 12 seconds after right-clicking to reload it with IE Tab. However, IE Tab can't be used for the Unicode version, since (like IE) it renders the fonts incorrectly.

-- Norm Megill

So if anyone uses this for greeting cards, it's going to be 1% DNA source material and 99% pre-conceived structure.

Almost all music generated from "natural" sources is like that, for example, the music generated by the digits of pi. If you take the digits of pi and convert them to a sequence of 10 pure MIDI tones, it would be very boring without the embellishment with elaborate orchestration.

There is at least one "natural" source, however, that bears some passing resemblance to "real" music: the patterns that occur in the proof trees of formal logic proofs. From the Metamath music page:

The music generated from these mathematical proofs stands in sharp contrast to certain other experimental music based on such mathematics as the digits of ? (pi). Unlike a proof's tree structure, which is inherently suggestive of a musical score, the digits of ? have no obvious pattern. To make it interesting, a human composer will often add a non-mathematical creative element such as an underlying beat with pre-selected chords and instrumentation. What one hears, then, might be based as much on the originality of the composer as on the essential nature of ?: the same algorithm applied to the digits of say e (Euler's constant), or even a series of random digits, would typically sound about the same after the first few notes. The music here, on the other hand, is a raw and unadorned representation of the mathematics itself, involving few human preconceptions beyond a basic mapping needed to accommodate the Western tonal scale.

It would be nice if they had a category for math and science, starting with the basics of math and building up. That is an interesting encoding problem in itself, to communicate that information independent of human context. For a start, a sequence of prime numbers might provide a clue that there is mathematical content in the information. Then, mathematics starting from axioms could be transmitted, (idealistically) building up to the general significant areas of modern mathematics. Imagine the reverse: supposed we received an alien transmission encoding proofs of outstanding Millenium prizes (P=NP, etc.) and much, much more. How could the alien communicate it to us, given that the alien would have zero knowledge of anything human?

I don't know the best format for presenting mathematical knowledge starting from a void, but the simplest language I know of that can encode all of modern mathematics directly along with rigorous proofs, is probably metamath. A 300-line program can verify its proofs (unlike about 3000 lines for other proof languages). I believe an intelligent human looking at its symbol strings in isolation, starting from the beginning, could probably figure out the encoding eventually, and presumably an intelligent alien could too. I think this would even be the case if you obfuscated all of its tokens with meaningless symbols - that is an important test. If I had a choice of one thing to transmit, it might be metamath's set theory database, probably with the human comments stripped out. (There are simpler universal languages such as SK combinatory logic, but they are not practical for expressing deep math theorems beyond a certain point.)

Similarly, it would be interesting to try to communicate physics from the ground up, starting with the axioms for what we know, and even eventually building up to chemistry and even biology. That might be a daunting and hopeless task, I don't know, but the problem of how to encode it is intriguing. Presumably math would come first, and physics would add its axioms and build on it. Or something like that.

(For the uninformed, consult Wikipedia. For a very precise breakdown of these axioms translated to primitve symbols - Wikipedia still includes some higher-level defined symbols that Wildberger objects to because he can't seem to understand them - see the metamath version. In other words, there is nothing fuzzy or ambiguous about these axioms.)

His set theory rant created quite a furor on Usenet, here and here.

Does anyone have a version of the proof that can be verified using the matamath proof explorer?

http://us2.metamath.org:8888/mpegif/mmset.html

Hey, don't knock it. Of all the sites on the web, OMG Ponies was one of the most noted. From "irina"'s blog: "This has been a particularly fun April Fool's... My favorite this year was Slashdot, with their 'OMG! Ponies!' theme. A close runner up was Poisson d'Avril's Theorem on Metamath."

By equality's transivity, yes! (Which means that the drug just got a lot easier to find...)

Gödel's theorem has another interpretation in the language of computer science. In first-order logic, theorems are recursively enumerable: you can write a computer program that will eventually generate any valid proof. You can ask if they have the stronger property of being recursive: can you write a computer program to definitively determine if a statement is true or false? Gödel's theorem says that in general you cannot.

Another thing to look at is Metamath music, which is interesting in a different way. It is the raw, unadorned piano music generated directly by mathematical proofs, very faithful to the actual mathematics.

Indeed, the Mayans had a symbol for their zero that looked something like a football.

I was talking about a different thing - that there is a similarity between proofs and algorithms; since it is usually not a big problem to translate a well-understood algorithm into a ("formal") program, I expect a similar process of formalizing a proof to be not much more difficult.

When "formalizing" an algorithm, you would normally use a high-level programming language rather than a machine code, and you would use libraries for, say, processing of text objects; the resulting program is usually not very big. Why would not you do something similar when formalizing a proof?

There have been some efforts in that direction; see, for example, metamath.

Jesus H. Christ, look at the context. We're talking about computer generated proofs that are too long to be verified by humans. The fact that a cosmic ray could cause a bit-flip and ruin a computation makes a purported proof not one until it is verified. Let alone the historical abundance of implementation bugs in software.

I've already seen computer generated proofs. These are easily verifiable, if tedious to do so. They are proofs. A sequence of sentences, computer generated or not, is not a proof until verified.

Now, before you go off and accuse people of magical thinking, you should learn a bit more literacy. Your characterization of my position is wildly incongruous with what I have written, in context. Kindly go fuck yourself next time you want to call someone irrational.

Here is a 300-line Python program that can verify the formal proof of any theorem (that can be proved from ZFC set theory axioms, which is essentially all of mathematics). So all you have to do is prove the correctness of these 300 lines, and the job is done. See us.metamath.org home page for more information on this program.