Cover Image

Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Linhares, Alexandre
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science 11A07 (Primary) 68V15, 11B65, 68T01 (Secondary) F.4.1; I.2.3; G.2.1
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Formalization of the Generalized Quantum Stein's Lemma in Lean
by: Meiburg, Alex, et al.
Published: (2025)

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

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

Project Synapse: A Hierarchical Multi-Agent Framework with Hybrid Memory for Autonomous Resolution of Last-Mile Delivery Disruptions
by: Yadav, Arin Gopalan, et al.
Published: (2026)

Learning to Repair Lean Proofs from Compiler Feedback
by: Wang, Evan, et al.
Published: (2026)

Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
by: Linhares, Alexandre
Published: (2026)

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

Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
by: Koomullil, George
Published: (2026)

Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
by: Ilin, Vasily
Published: (2026)

Softly Constrained Denoisers for Diffusion Models Applied to Partial Differential Equations
by: Yeom-Song, Victor M., et al.
Published: (2025)

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

LTL Verification of Memoryful Neural Agents
by: Hosseini, Mehran, et al.
Published: (2025)

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

Complex Facial Expression Recognition Using Deep Knowledge Distillation of Basic Features
by: Maiden, Angus, et al.
Published: (2023)

Recent Advances in Data-Driven Business Process Management
by: Ackermann, Lars, et al.
Published: (2024)

AgentLeak: A Full-Stack Benchmark for Privacy Leakage in Multi-Agent LLM Systems
by: Yagoubi, Faouzi El, et al.
Published: (2026)

Partitioned Neural Network Training via Synthetic Intermediate Labels
by: Karadağ, Cevat Volkan, et al.
Published: (2024)

On measuring grounding and generalizing grounding problems
by: Quigley, Daniel, et al.
Published: (2025)

Safe Distributed Control of Multi-Robot Systems with Communication Delays
by: Ballotta, Luca, et al.
Published: (2024)

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

A correspondence between the time and space complexity
by: Latkin, Ivan V.
Published: (2023)

Formalizing Computational Paths and Fundamental Groups in Lean
by: Ramos, Arthur F., et al.
Published: (2025)

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

FedRot-LoRA: Mitigating Rotational Misalignment in Federated LoRA
by: Zhang, Haoran, et al.
Published: (2026)

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

Deep Neural Networks with General Activations: Super-Convergence in Sobolev Norms
by: Yang, Yahong, et al.
Published: (2025)

Determination of the fifth Busy Beaver value
by: The bbchallenge Collaboration, et al.
Published: (2025)

From Particles to Agents: Hallucination as a Metric for Cognitive Friction in Spatial Simulation
by: Sánchez-Vaquerizo, Javier Argota, et al.
Published: (2026)

Synthetic data for ratemaking: imputation-based methods vs adversarial networks and autoencoders
by: Havrylenko, Yevhen, et al.
Published: (2025)

AI LLM Proof of Self-Consciousness and User-Specific Attractors
by: Camlin, Jeffrey
Published: (2025)

Model Callers for Transforming Predictive and Generative AI Applications
by: Dalal, Mukesh
Published: (2024)

Quantifying Behavioral Dissimilarity Between Mathematical Expressions
by: Mežnar, Sebastian, et al.
Published: (2024)

Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
by: Echenim, Mnacho, et al.
Published: (2023)

FedUNet: A Lightweight Additive U-Net Module for Federated Learning with Heterogeneous Models
by: Seo, Beomseok, et al.
Published: (2025)

Complete Robust Hybrid Systems Reachability
by: Wafa, Noah Abou El, et al.
Published: (2026)

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

Large Language Models in Software Documentation and Modeling: A Literature Review and Findings
by: Radosky, Lukas, et al.
Published: (2026)

Ethical AI Governance: Methods for Evaluating Trustworthy AI
by: McCormack, Louise, 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)