John J. Harrison, Amazon Web Services, Portland, OR 97201

• ArXiv (3): A formal proof of the Kepler conjecture, 2015\
• Homepage(s): Cambridge, dblp, Github
• Publications: Handbook of Practical Logic and Automated Reasoning, Cambridge University Press 2009; Theorem Proving with the Real Numbers, Springer-Verlag, 1998.

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 for disintermediating space and time (ever-so-slowly). 

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 July 11 at 10:28 AM!

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

Warmly,

Bruce