Cover Image

Algorithm and abstraction in formal mathematics

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Macbeth, Heather
Format:	Preprint
Published:	2024
Subjects:	History and Overview 68V20 (Primary) 00A30, 03B35, 68-02, 68V15 (Secondary) F.4.1
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

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

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

Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization
by: Incatasciato, Guillermo L., et al.
Published: (2024)

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

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

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

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

Leveraging guidelines for ethical practice of statistics and computing to develop standards for ethical mathematical practice: A White Paper
by: Buell, Catherine, et al.
Published: (2022)

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

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)

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

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

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

The extension of zbMATH Open by arXiv preprints
by: Beckenbach, Isabel, et al.
Published: (2024)

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

A novel approach to the relationships between data features -- based on comprehensive examination of mathematical, technological, and causal methodology
by: Kim, JaeHong
Published: (2025)

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

Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)
by: Nakano, Keisuke, et al.
Published: (2024)

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

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

A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes
by: Bruse, Florian, et al.
Published: (2026)

Hilbert's Program and Infinity
by: Zach, Richard
Published: (2026)

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

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

The Network Structure of Mathlib
by: Li, Xinze, et al.
Published: (2026)

Conformance Checking of Fuzzy Logs against Declarative Temporal Specifications
by: Donadello, Ivan, et al.
Published: (2024)

Universal truth of operator statements via ideal membership
by: Hofstadler, Clemens, et al.
Published: (2022)

Astrolabe: A Content-Addressable Hypergraph for Semantic Knowledge Management
by: Li, Xinze
Published: (2026)

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

A Logspace Constructive Proof of L=SL
by: Buss, Sam, et al.
Published: (2025)

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

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

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

Proof complexity of universal algebra in a CSP dichotomy proof
by: Gaysin, Azza
Published: (2024)

Why the classes P and NP are not well-defined finitarily
by: Anand, Bhupinder Singh
Published: (2024)

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