Elamur Research⌕
☰
home / authors / John Harrison

John Harrison

John Harrison has 2 papers in our library, in 2014–2015, most of them on Reasoning; often with Cezary Kaliszyk, Josef Urban, Tobias Nipkow.

2 papers in our library · 2014–2015

OpenAlex · ORCID · h-index 36 · 102 works · 4,026 citations OpenAlex, 2026-10-14

📄 2 works in our library · 🔗 Cited 45 times in our library · ⭐ Paper Stars ranking: #6889

The profile is the library's match of the name; two people with one name are not always told apart.

Elsewhere: Google Scholar · Semantic Scholar · dblp · ACL Anthology

 Affiliations

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 2 more institutions on single bylines are not listed.

 Fields, topics and concepts

Of its works in our library, with the number of works on each.

 Works by year

2010s

 Papers

The most cited first (OpenAlex and our library).

  1. History of Interactive Theorem Proving (2014 · 109 citations)
    This book chapter traces the history of formal proof built through human–machine cooperation, as opposed to proving done entirely by the computer.
  2. A formal proof of the Kepler conjecture (2015 · 79 citations)
    The Kepler conjecture claims that no arrangement of equal balls in three-dimensional space is denser than the face-centered cubic packing, whose density is π/√18 (about 0.74).

 Co-authors here

3 co-authors with a page, the most papers together first.

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

 Cited by

Papers of our library cite their works 45 times (of the 149,439 papers whose bibliographies we read); 27 citing papers with a page here →.

Updated

This page in Markdown → https://md.research.elamur.ai/free/en/authors/john-harrison/