PeopleofSuperintelligence

Researcher

Henrik Böving

Also known as hargoniX

Henrik Böving is a research software engineer at the Lean FRO who builds verified automation for the Lean proof assistant, including bv_decide, a tactic for solving fixed-width bitvector goals. They began their doc-gen4 documentation project for Lean 4 in September 2021 and were a dual student at Hochschule München by February 2022. With coauthors including Siddharth Bhat, Clark Barrett and Tobias Grosser, they presented bv_decide in an October 2025 OOPSLA paper as the first end-to-end verified bitblaster for interactive bitvector reasoning in a dependently typed interactive theorem prover, and the tactic competed at SMT-COMP in 2025 and 2026. At FLoC 2026 in July 2026, Leo de Moura reported their port of bv_decide to SymM and argued that better tactics make more powerful AI, noting that every medal-level IMO AI with formal proofs uses Lean.

Timeline

  1. April 2020

    An embedded Rust driver

    In April 2020, they publish a tutorial on writing a Rust driver for the AT42QT1070 touch sensor on a credit-card-sized board controlled by an STM32L4 microcontroller.

  2. 2021–2022

    Starting doc-gen4

    In September 2021, they offer to write a doc-gen-style documentation tool for Lean 4, the start of their doc-gen4 project. By February 2022, they are a dual student at Hochschule München who lives and works just east of Munich.

  3. By 2023

    A Lean 4 metaprogramming book

    By August 2023, they are one of eight authors of A Lean 4 Metaprogramming Book, a community textbook on GitHub that Arthur Paulino initiated. The other authors are Damiano Testa, Edward Ayers, Evgenia Karunus, Jannis Limperg, Siddhartha Gadgil and Siddharth Bhat.

  4. January 2025

    bv_decide at Lean Together

    In January 2025, they give a Lean Together 2025 talk for the Lean FRO on bv_decide, a tactic for solving all fixed-width BitVec goals, covering its inner workings, a performance evaluation and real-world applications.

  5. 2025

    Entering SMT-COMP 2025

    Their tactic enters SMT-COMP 2025, the International Satisfiability Modulo Theories Competition, in two versions, bv_decide and bv_decide-nokernel, with Böving first among eleven contributors.

  6. October 2025

    An OOPSLA paper on bit-blasting

    In October 2025, they publish “Interactive Bitvector Reasoning using Verified Bit-Blasting” as first author, with coauthors including Siddharth Bhat, Clark Barrett and Tobias Grosser, in the OOPSLA2 issue of Proceedings of the ACM on Programming Languages. The paper presents bv_decide as the first end-to-end verified bitblaster for interactive bitvector reasoning in a dependently typed interactive theorem prover and verifies over 7000 SMT statements extracted from LLVM. They present the work for the Lean FRO at SPLASH 2025 in Singapore.

  7. 2026

    Porting bv_decide to SymM

    SMT-COMP 2026 again includes bv_decide, with Böving first among its contributors. In July 2026, at FLoC 2026 in Lisbon, Leo de Moura reports that Böving has ported bv_decide to SymM, where it solves 45,046 of 46,191 SMT-LIB bit-vector problems with kernel checking included. The talk argues that better tactics make more powerful AI and notes that every medal-level IMO AI with formal proofs uses Lean.

  8. As of October 2026

    Research software engineer at Lean FRO

    They are a research software engineer at the Lean FRO, working on verified decision procedures, code generation and performance optimizations in Lean 4. In September 2026, they publish a guide to Array.markLinear, which helps developers find linearity bugs that force Lean to copy data structures it could update in place.

  1. Google had the most people shaping AI every year from 2014 to 2025Our estimates of which organizations employed the most people shaping AI from 1961 to 2025, with a year-by-year chart.
  2. The United States employs an estimated 53% of people in our data with a known employment countryOur estimates of where AI careers are concentrated now and how countries’ shares of dated positions changed over time.
  3. 46% of living people in our data with known birth and employment countries work outside their birth countryOur estimate of cross-border careers in AI, from country of birth and the country of each current organization.
  4. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionOur estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Henrik Böving yet. Send us a free-licensed photo.

  1. Writing embedded drivers in Rust isn't that hard. Part 1 hboeving.dev. Checked 19 October 2026.
  2. Zulip Chat Archive: lean4, doc-gen4 leanprover-community.github.io. Checked 19 October 2026.
  3. Zulip Chat Archive: Geographic locality, Munich, DE leanprover-community.github.io. Checked 19 October 2026.
  4. GitHub - leanprover-community/lean4-metaprogramming-book github.com. Checked 19 October 2026.
  5. Zulip Chat Archive: lean4, Citation for the metaprogramming book leanprover-community.github.io. Checked 19 October 2026.
  6. Automated Bit-Level Reasoning in Lean 4 (Lean Together 2025) researchseminars.org. Checked 19 October 2026.
  7. Participants | SMT-COMP 2025 smt-comp.github.io. Checked 19 October 2026.
  8. Interactive Bitvector Reasoning using Verified Bit-Blasting theory.stanford.edu. Checked 19 October 2026.
  9. Interactive Bit Vector Reasoning using Verified Bitblasting (SPLASH 2025 - OOPSLA) 2025.splashcon.org. Checked 19 October 2026.
  10. Participants | SMT-COMP 2026 smt-comp.github.io. Checked 19 October 2026.
  11. The Lean Theorem Prover: Design, Evolution, and Impact leodemoura.github.io. Checked 19 October 2026.
  12. Team — Lean FRO lean-lang.org. Checked 19 October 2026.
  13. About — Henrik Böving hboeving.dev. Checked 19 October 2026.
  14. Dynamically Identifying Linearity Bugs in Lean 4 hboeving.dev. Checked 19 October 2026.