Copertina

Remote Verification System for Mizar Integrated with Emwiki

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Kai, Toshiki, Teruya, Yuta, Nakasho, Kazuhisa
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Software Engineering 68V05, 68V15, 68V20, 68V30, 68V35 G.4
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Formalizing Pick's Theorem, efficiently
di: Eisermann, Michael
Pubblicazione: (2026)

Algorithm and abstraction in formal mathematics
di: Macbeth, Heather
Pubblicazione: (2024)

Formalising New Mathematics in Isabelle: Diagonal Ramsey
di: Paulson, Lawrence C
Pubblicazione: (2025)

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

Anatomy of a Formal Proof
di: Avigad, Jeremy, et al.
Pubblicazione: (2024)

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

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

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

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

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

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

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

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

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

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

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

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

MaRDIFlow: A CSE workflow framework for abstracting meta-data from FAIR computational experiments
di: Veluvali, Pavan L., et al.
Pubblicazione: (2024)

Towards Semantic Markup of Mathematical Documents via User Interaction
di: Vrečar, Luka, et al.
Pubblicazione: (2024)

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

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

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

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

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

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

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

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

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

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

A formalization of Borel determinacy in Lean
di: Manthe, Sven
Pubblicazione: (2025)

Self-adhesivity in lattices of abstract conditional independence models
di: Boege, Tobias, et al.
Pubblicazione: (2024)

Hyperstability in the Erdős-Sós Conjecture
di: Pokrovskiy, Alexey
Pubblicazione: (2024)

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

Bounding the density of binary sphere packing
di: Fernique, Thomas, et al.
Pubblicazione: (2025)

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

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

The minimal volume of stable surfaces of rank one
di: Liu, Jihao, et al.
Pubblicazione: (2026)

Utilizing redundancies in Qubit Hilbert Space to reduce entangling gate counts in the Unitary Vibrational Coupled-Cluster Method
di: Szczepanik, Michal, et al.
Pubblicazione: (2024)

A Formally Verified Library of Mathematical Finance in Lean 4
di: Coelho, Raphael
Pubblicazione: (2026)

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