Oscar Fitzharding

Years active
2026

Resources

Repositorysq19

By Fitzharding

github.com/ofitzharding/sq19A Lean 4 proof that Wainwright's packing of nineteen squares is optimal, trusting Lean's compiler for its certificates.

1 result (at S5) · 1 record (at S5)

Repositorysq17-lean

By Fitzharding

github.com/ofitzharding/sq17-leanA Lean 4 proof that Bidwell's packing of seventeen squares is optimal, trusting Lean's compiler for its certificates.

1 result (at S5) · 1 record (at S5)

2 results (at S5) · 2 records (at S5) · 0 credits

Results

  • T-154 (formalization, n = 17): source author, credited contributor — Fitzharding, in [Fitzharding n17 Lean 2026] (Registered in: #592 · #595 · #588)
  • T-194 (optimality, n = 19): source author, credited contributor — Fitzharding, in [Fitzharding n19 Lean 2026]

Records

Current registered contributions in their recorded family and scope. A result counts once when any of its facets remains current.

  • T-154 (formalization, n = 17): source author, credited contributor — Fitzharding, in [Fitzharding n17 Lean 2026] (Registered in: #592 · #595 · #588)
  • T-194 (optimality, n = 19): source author, credited contributor — Fitzharding, in [Fitzharding n19 Lean 2026]

Related News

Sources
  1. citation-cff: authors gives given-names Oscar and family-names Fitzharding; repository-code is github.com/ofitzharding/sq17-lean.
  2. licence: MIT licence, “Copyright (c) 2026 Oscar Fitzharding”.
  3. packet: Opening paragraphs: the author Oscar Fitzharding announced the proof on X as @ofitzharding, and the owner set Oscar Fitzharding as the definitive name. Source and Pin table: author and committer ofitzharding; issue #565 opened by ofitzharding.
  4. announcement: The post of 2026-10-13T00:06:56Z from @ofitzharding (display name “Oscar”, account 2097726704118603776) announcing the first complete Lean proof of optimality for Bidwell’s 1998 packing of 17 squares.
  5. release-readme: Credits and the closing note: “This project was developed with substantial assistance from Claude and Codex.”
  6. bibliography: credited_names maps Oscar Fitzharding to Fitzharding; the [Fitzharding n17 Lean 2026] entry credits Fitzharding.

Identity evidence