<div>My friend Landon sent me the link I needed to say "math proves that math is equivalent to programming"; it actually says something more like "there is an isomorphism between proofs of deductive logic and constructions of Lambda Calculus" but even that I'm saying badly, the link is 
<a href="http://en.wikipedia.org/wiki/Curry-Howard_isomorphism">http://en.wikipedia.org/wiki/Curry-Howard_isomorphism</a></div>
<div>Gratifyingly, the intro has the phrase "Proofs are Programs" :-)</div>
<div> </div>
<div>On second thought my guestimate of the size of a program that might be produced from the Clasification of Finite Simple Groups is excessive. I'm thinking 100MB would be more fair order of magnitude than 1GB.</div>

<div> </div>
<div>I don't mean that the possible huge size of source code justifies 64 bit words, it's enough, to me, that a huge integer can fit into a register, for number theory. But yes we humans can indeed create vast grotesque edifices of scholarship without the necessity of machine generation.
</div>
<div> </div>
<div>But the machines will, of course, win in the end :-)</div>
<div> </div>
<div>Peter<br><br> </div>
<div><span class="gmail_quote">On 4/11/07, <b class="gmail_sendername">Peter St. John</b> <<a href="mailto:peter.st.john@gmail.com">peter.st.john@gmail.com</a>> wrote:</span>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">Jon,<br><br>
<div><span class="q"><span class="gmail_quote">On 4/10/07, <b class="gmail_sendername">Jon Forrest</b> <<a onclick="return top.js.OpenExtLink(window,event,this)" href="mailto:jlforrest@berkeley.edu" target="_blank">jlforrest@berkeley.edu
</a>> wrote:</span> 
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid"><br>But I stand firm on my claim that no human, or group<br>of humans, can write a program that requires more than 
<br>32-bits of text space.</blockquote>
<div> </div></span>
<div>I like to say that proving a theorem is alot like writing a program. I don't know about the biggest software projects, but the Classification of  Finite Simple Groups was huge; from Wiki:</div>
<div>"In all, the work comprises tens of thousands of pages in 500 journal articles by some 100 authors."</div>
<div>My thumbnail guesstimate of how much bytes are in a typical journal page of mathematics (maybe less than AMSTeX source, but more than 2k of plaintext prose, because all the symbols have to be expressed as abbreivations...) suggests that this work, done by humans, amounts to more than 4 GB. 
</div>
<div>I'm not clear, myself, about the "infinite flat address space", as I want my data space to be a bit more structured (in my view of the C source, say) and don't want to care about how it looks to the compiler (as long as the compiler is happy). However,  the killer app to me is what RGB mentioned; I know and love numbers that don't fit in one 32-bit word. 
</div><span class="sg">
<div>Peter</div></span><span class="q"><br>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">Cordially,<br>--<br>Jon Forrest<br>Unix Computing Support<br>College of Chemistry<br>173 Tan Hall<br>University of California Berkeley 
<br>Berkeley, CA<br>94720-1460<br>510-643-1032<br><a onclick="return top.js.OpenExtLink(window,event,this)" href="mailto:jlforrest@berkeley.edu" target="_blank">jlforrest@berkeley.edu</a><br>_______________________________________________
<br>Beowulf mailing list, <a onclick="return top.js.OpenExtLink(window,event,this)" href="mailto:Beowulf@beowulf.org" target="_blank">Beowulf@beowulf.org</a><br>To change your subscription (digest mode or unsubscribe) visit 
<a onclick="return top.js.OpenExtLink(window,event,this)" href="http://www.beowulf.org/mailman/listinfo/beowulf" target="_blank">http://www.beowulf.org/mailman/listinfo/beowulf</a><br></blockquote></span></div><br></blockquote>
</div><br>