Imagen de Portada

Formalizing Pick's Theorem, efficiently

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autor principal:	Eisermann, Michael
Formato:	Preprint
Publicado:	2026
Materias:	Geometric Topology 68V15, 68V20
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Formalizing Pick's Theorem in Isabelle/HOL
por: Binder, Sage, et al.
Publicado: (2024)

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

Anatomy of a Formal Proof
por: Avigad, Jeremy, et al.
Publicado: (2024)

Formalising New Mathematics in Isabelle: Diagonal Ramsey
por: Paulson, Lawrence C
Publicado: (2025)

The number of primitive words of unbounded exponent in the language of an HD0L-system is finite
por: Klouda, Karel, et al.
Publicado: (2021)

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

Algorithm and abstraction in formal mathematics
por: Macbeth, Heather
Publicado: (2024)

Evolving Ranking Functions for Canonical Blow-Ups in Positive Characteristic
por: Bérczi, Gergely
Publicado: (2026)

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

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

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

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

Primal-Dual Coordinate Descent for Nonconvex-Nonconcave Saddle Point Problems Under the Weak MVI Assumption
por: Walwil, Iyad, et al.
Publicado: (2025)

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

Evolving Local Corrections for Global Constructions in Combinatorics
por: Bérczi, Gergely
Publicado: (2026)

Advancing Mathematical Research via Human-AI Interactive Theorem Proving
por: Li, Chenyi, et al.
Publicado: (2025)

Classification of Covering Spaces and Canonical Change of Basepoint
por: Wemmenhove, Jelle, et al.
Publicado: (2024)

Formalizing Polynomial Laws and the Universal Divided Power Algebra
por: Chambert-Loir, Antoine, et al.
Publicado: (2025)

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

Graph2Tac: Online Representation Learning of Formal Math Concepts
por: Blaauwbroek, Lasse, et al.
Publicado: (2024)

Word-length curve counting on the once-punctured torus
por: Fisac, David, et al.
Publicado: (2024)

Geometric Meta-Learning via Coupled Ricci Flow: Unifying Knowledge Representation and Quantum Entanglement
por: Lei, Ming, et al.
Publicado: (2025)

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

Efficient computation of stationary measures and the Lyapunov Landscape for families random dynamical systems with smooth additive noise
por: Galatolo, Stefano, et al.
Publicado: (2025)

The complexity of pinning simple multiloops
por: Seo, Eric, et al.
Publicado: (2026)

Flow-based Extremal Mathematical Structure Discovery
por: Bérczi, Gergely, et al.
Publicado: (2026)

PatternBoost: Constructions in Mathematics with a Little Help from AI
por: Charton, François, et al.
Publicado: (2024)

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

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

LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
por: Peyronnet, Antoine, et al.
Publicado: (2026)

Optimal strategies in the all-heads coin game
por: Pfaffelhuber, Peter
Publicado: (2026)

A formalization of Borel determinacy in Lean
por: Manthe, Sven
Publicado: (2025)

Detecting random bifurcations via rigorous enclosures of large deviations rate functions
por: Blessing, Alexandra, et al.
Publicado: (2024)

Formalization in Lean of faithfully flat descent of projectivity
por: Shaul, Liran
Publicado: (2026)

Quasi-Sturmian colorings on regular trees
por: Kim, Dong Han, et al.
Publicado: (2018)

The spherical growth series of amalgamated free products of infinite cyclic groups
por: Fujii, Michihiko, et al.
Publicado: (2025)

On sequential versions of distributional topological complexity
por: Jauhari, Ekansh
Publicado: (2024)

The best possible constants approach for Wilker-Cusa-Huygens inequalities via stratification
por: Banjac, Bojan, et al.
Publicado: (2024)

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

Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
por: Linhares, Alexandre
Publicado: (2026)