Copertina

Munkres' General Topology Autoformalized in Isabelle/HOL

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Bryant, Dustin, Munive, Jonathan Julián Huerta y, Kaliszyk, Cezary, Urban, Josef
Natura:	Preprint
Pubblicazione:	2026
Soggetti:	Artificial Intelligence Machine Learning Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Verifying Numerical Methods with Isabelle/HOL
di: Bryant, Dustin, et al.
Pubblicazione: (2025)

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
di: Brown, Chad E., et al.
Pubblicazione: (2026)

130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
di: Urban, Josef
Pubblicazione: (2026)

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
di: Munive, Jonathan Julián Huerta y, et al.
Pubblicazione: (2024)

Learning Guided Automated Reasoning: A Brief Survey
di: Blaauwbroek, Lasse, et al.
Pubblicazione: (2024)

Exploring Formal Math on the Blockchain: An Explorer for Proofgold
di: Brown, Chad E., et al.
Pubblicazione: (2025)

Payment Channels with Proofs
di: Brown, Chad E., et al.
Pubblicazione: (2025)

Autoformalizing Euclidean Geometry
di: Murphy, Logan, et al.
Pubblicazione: (2024)

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
di: Zhang, Liao, et al.
Pubblicazione: (2024)

Linear Programming in Isabelle/HOL
di: Parsert, Julian
Pubblicazione: (2024)

Differentiable Inductive Logic Programming in High-Dimensional Space
di: Purgał, Stanisław J., et al.
Pubblicazione: (2022)

Hammering Higher Order Set Theory
di: Brown, Chad E., et al.
Pubblicazione: (2025)

SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization
di: Su, Xiaole, et al.
Pubblicazione: (2026)

Machine Learning for Quantifier Selection in cvc5
di: Jakubův, Jan, et al.
Pubblicazione: (2024)

Solving Hard Mizar Problems with Instantiation and Strategy Invention
di: Jakubův, Jan, et al.
Pubblicazione: (2024)

Brownian Motion in Isabelle/HOL
di: Laursen, Christian Pardillo, et al.
Pubblicazione: (2024)

Learning Conjecturing from Scratch
di: Gauthier, Thibault, et al.
Pubblicazione: (2025)

Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection
di: Lalwani, Abhinav, et al.
Pubblicazione: (2024)

Complex Bounded Operators in Isabelle/HOL
di: Unruh, Dominique, et al.
Pubblicazione: (2025)

Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
di: Pąk, Karol, et al.
Pubblicazione: (2024)

Can Large Language Models Autoformalize Kinematics?
di: Kabra, Aditi, et al.
Pubblicazione: (2025)

Experiments with Choice in Dependently-Typed Higher-Order Logic
di: Ranalter, Daniel, et al.
Pubblicazione: (2024)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
di: Bartl, Lukas, et al.
Pubblicazione: (2025)

Automated Strategy Invention for Confluence of Term Rewrite Systems
di: Zhang, Liao, et al.
Pubblicazione: (2024)

Proof Recommendation System for the HOL4 Theorem Prover
di: Dekhil, Nour, et al.
Pubblicazione: (2024)

Stalnaker's Epistemic Logic in Isabelle/HOL
di: Guzman, Laura P. Gamboa, et al.
Pubblicazione: (2024)

Formalization of Differential Privacy in Isabelle/HOL
di: Sato, Tetsuya, et al.
Pubblicazione: (2024)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
di: Foster, Simon, et al.
Pubblicazione: (2024)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
di: Stübinger, Terru, et al.
Pubblicazione: (2023)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
di: Niederhauser, Johannes, et al.
Pubblicazione: (2024)

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
di: Hulak, David B., et al.
Pubblicazione: (2026)

ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
di: Cabral, Rafael, et al.
Pubblicazione: (2025)

Process-Driven Autoformalization in Lean 4
di: Lu, Jianqiao, et al.
Pubblicazione: (2024)

A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
di: Li, Chunxiao, et al.
Pubblicazione: (2024)

Inductive Generalization in Reinforcement Learning from Specifications
di: Subramanian, Vignesh, et al.
Pubblicazione: (2024)

Logic Tensor Network-Enhanced Generative Adversarial Network
di: Upreti, Nijesh, et al.
Pubblicazione: (2026)

Most General Explanations of Tree Ensembles (Extended Version)
di: Izza, Yacine, et al.
Pubblicazione: (2025)

MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
di: Liu, Xinyu, et al.
Pubblicazione: (2026)

Procedural Adherence and Interpretability Through Neuro-Symbolic Generative Agents
di: Rothkopf, Raven, et al.
Pubblicazione: (2024)

MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs
di: Pati, Viresh, et al.
Pubblicazione: (2026)