Upon following the work of John J. Harrison

TO: John J. Harrison, Amazon Web Services, Portland, OR 97201
FM: Bruce E. Camber
RE: Of your arXiv articles, A formal proof of the Kepler conjecture (2015); even your homepages are helpful on Cambridge, dblp, and Github, Your other publications, i.e. your Handbook of Practical Logic and Automated Reasoning, Cambridge University Press 2009 and your Theorem Proving with the Real Numbers, Springer-Verlag, 1998 are also helpful.

URL for this page: https://81018.com/harrison/

First email: 11 July 2022 at 10:28 AM

Dear John:

How entirely moving to find HOL Light within the Thomas Hales’ work to create a foundation of logic to treat Kepler’s Conjecture. To find Cambridge university hosting HOL Light, and with you at Amazon Web Services in Portland,  it was a pleasant non sequitur and a sign of our time — ever so slowly disintermediating space and time.

I immediately went looking for your use and explanation of pi (π).  So, I am now exploring deeper into HOL Light and I thought you would be amused how somebody finds you and immediately gravitates to your work. Thank you.

BTW, I am modestly trying to figure out the most-simple starting point for the universe. We started in a high school geometry class going inside the tetrahedron, the octahedron with it, and then the tetrahedrons (8) and octahedrons (6) within it. Planck’s base units suggested we go no further. That was 112 base-2 jumps from the classroom. Multiplying by 2, we were out 90 more jumps to the edges of the universe and the current time: https://81018.com/chart/

So, if we assume Planck’s calculations are in the ballpark, those 202 notations encapsulate everything, everywhere for all time. That is sweet, but what does the first instant look like?

Because a friend at Brown and former NIST head mathematician (back when it was the National Bureau of Standards) and I argued about it, I settled with him and went with his sphere. 

So, I’ll wrestle around and try to figure out why HOL Light makes light of the sphere and pi. That’s a nice exercise for 11 July 2022 at 10:28 AM!

Thanks again for all that you do to make our world a better place

Warmly,

Bruce

###