Javier Burroni
  • about
  • publications
  • blog(current)
  • cv
  • IWAE
  • •

  • VI
  • •

  • low-level
  • •

  • research
  • •

  • lean
  • rintro and A ≠ B

    Using rintro to simplify derivations of A ≠ B in Lean

    3 min read   ·   July 14, 2025

    2025   ·   Lean,   Lean-snippets,   formalization,   tactics,   rintro     ·   lean  

  • Understanding the Suffices Tactic in Lean

    A small pattern I noticed in Lean proofs that can be simplified using the `suffices` tactic.

    5 min read   ·   July 07, 2025

    2025   ·   Lean,   Lean-snippets,   formalization,   tactics,   suffices,   fin_cases     ·   lean  

  • Vibe coding

    I found a complete program that GPT wrote for me, more than two years ago.

    2 min read   ·   June 30, 2025

    2025   ·   vibe   coding,   AI,   GPT     ·   AI  

  • Formalizing Length Functions in Coding Theory

    A brief discussion on the formalization of length functions, which are more than just a mapping from elements of an alphabet to natural numbers. They also need to satisfy a capacity bound condition.

    7 min read   ·   June 11, 2025

    2025   ·   Lean,   Lean-snippets,   formalization,   numbers     ·   lean  

  • Using numbers, real numbers, in Lean

    Having a calculation with real numbers in Lean is not as straightforward as it seems. I'm sure I'll learn better ways to do it in the future, but for now, I want to share how I solved this problem.

    3 min read   ·   June 05, 2025

    2025   ·   Lean,   Lean-snippets,   formalization,   numbers     ·   lean  

  • Newer
  • 1
  • 2
  • Older
© Copyright 2025 Javier Burroni. Powered by Jekyll with al-folio theme. Hosted by GitHub Pages. Last updated: July 14, 2025.