Grant Olney Passmore's photo  

Dr. Grant Olney Passmore



Researcher, Automated Theorem Proving and Formal Verification

Co-Founder and Co-CEO,
Aesthetic Integration, London

Life Member,
Clare Hall, University of Cambridge

AI HQ: +44 (0)20-3773-6225

Aesthetic Integration, Ltd.
1 Fore St.
City of London


New Course on Algebro-Geometric Decision Methods at Cambridge

  • During Lent term, 2012, I taught a Part IV pure mathematics course called Decision Methods over Real and Algebraically Closed Fields at DPMMS, Cambridge. I had a wonderful time and am very keen to teach such a course again. Please let me know if you'd like the notes (feedback appreciated!). Thank you to those of you who joined! (A rough lecture roadmap, beginning with Lecture 1 - `Framing the Miracle' of the decidability of Th(<R, +, *, <, 0, 1>), and ending with Lecture 10 - `Krivine-Stengle Weak Positivstellensatz')


  • Reznick's moving ``The Secret Lives of Polynomial Identities'' : pdf
  • Kuga's indescribable ``Galois' Dream: Group Theory and Differential Equations'' : Google Books preview ; truly a work of beauty
  • Leon Henkin's riveting 1996 article ``The Discovery of My Completeness Proofs''; when constants are enough ~ completeness for FOL on the way to completeness for HOL (w.r.t. general models)!
  • Natalie Wolchover's wonderful 2013 article ``In Computers We Trust?'' on the use of computers in both discovery and proof in mathematics
  • Instrument - Ten Years of the Band Fugazi : imdb ; nevermind what's been selling, it's what you're buying
  • Killing a Camera - The Braid Documentary : insound ; new nathan detroits!
  • Björk interviewing Arvo Pärt : YouTube (i, ii)
  • Paul Cohen on his relationship with Gödel and the discovery of forcing : YouTube (i, ii, iii, iv, v, vi) ; beyond words
  • The work of Alex Wilkie
  • Real algebraic and analytic geometry preprint server
  • Model theory preprint server
  • The films (mysteries!) of Michaelangelo Antonioni