Cover Image

Formalizing Pick's Theorem in Isabelle/HOL

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Binder, Sage, Kosaian, Katherine
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science 03B35, 68V15, 68V20 F.3.1
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
by: Wang, Zili, et al.
Published: (2025)

Anatomy of a Formal Proof
by: Avigad, Jeremy, et al.
Published: (2024)

Formalising New Mathematics in Isabelle: Diagonal Ramsey
by: Paulson, Lawrence C
Published: (2025)

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
by: Farmer, William M.
Published: (2026)

A Modular First Formalisation of Combinatorial Design Theory
by: Edmonds, Chelsea, et al.
Published: (2021)

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
by: Edmonds, Chelsea, et al.
Published: (2023)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
by: Farmer, William M., et al.
Published: (2023)

A Higher-Order Vampire (Short Paper)
by: Bhayat, Ahmed, et al.
Published: (2024)

Internalizing Extensions in Lattices of Type Theories
by: Chan, Jonathan
Published: (2025)

Bounded First-Class Universe Levels in Dependent Type Theory
by: Chan, Jonathan, et al.
Published: (2025)

Formalizing Pick's Theorem, efficiently
by: Eisermann, Michael
Published: (2026)

Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
by: Zhang, Manqing, et al.
Published: (2026)

Universal Algebra in UniMath
by: Amato, Gianluca, et al.
Published: (2021)

A new decision method for Intuitionistic Logic by 3-valued non-deterministic truth-tables (pre-print version)
by: Leme, Renato, et al.
Published: (2023)

Virasoro algebra and Sugawara constructions formally in Lean
by: Kytölä, Kalle
Published: (2025)

Remarks on Primitive Regulation
by: Rosko, Milan
Published: (2026)

Algorithm and abstraction in formal mathematics
by: Macbeth, Heather
Published: (2024)

Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
by: Lau, Gabriel Rongyang
Published: (2026)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
by: Linzi, Alessandro
Published: (2025)

Mechanised uniform interpolation for modal logics K, GL, and iSL
by: Férée, Hugo, et al.
Published: (2024)

Artifical intelligence and inherent mathematical difficulty
by: Dean, Walter, et al.
Published: (2024)

A formalization of Borel determinacy in Lean
by: Manthe, Sven
Published: (2025)

Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation
by: Alpay, Faruk, et al.
Published: (2025)

Higher-Order Pattern Unification Modulo Similarity Relations
by: Dundua, Besik, et al.
Published: (2025)

A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking
by: Wang, Shuai
Published: (2024)

The continuous functional calculus in Lean
by: Dedecker, Anatole, et al.
Published: (2025)

A Formal Analysis of Algorithms for Matroids and Greedoids
by: Abdulaziz, Mohammad, et al.
Published: (2025)

The Solver's Paradox in Formal Problem Spaces
by: Rosko, Milan
Published: (2025)

Single-set cubical categories and their formalisation with a proof assistant (extended version)
by: Malbos, Philippe, et al.
Published: (2024)

An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
by: Martina, Antoine, et al.
Published: (2023)

Domains, Information Frames, and Their Logic
by: Spreen, Dieter
Published: (2025)

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
by: Firsching, Moritz, et al.
Published: (2026)

Remote Verification System for Mizar Integrated with Emwiki
by: Kai, Toshiki, et al.
Published: (2024)

A Formalization of Abstract Rewriting in Agda
by: Arkle, Sam, et al.
Published: (2026)

Combining Mechanical and Agentic Specification Inference for Move
by: Grieskamp, Wolfgang, et al.
Published: (2026)

Normative Conditional Reasoning as a Fragment of HOL
by: Parent, Xavier, et al.
Published: (2023)

Nominal techniques as an Agda library
by: Gabbay, Murdoch J., et al.
Published: (2026)

Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
by: Wiesnet, Franziskus
Published: (2025)

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
by: Ramos, Arthur, et al.
Published: (2025)