Cover Image

Synthetic Differential Geometry in Lean

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Brasca, Riccardo, Clemente, Gabriella
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Differential Geometry
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
by: Hulak, David B., et al.
Published: (2026)

Real Einstein loci
by: Clemente, Gabriella
Published: (2025)

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
by: Huang, Yihe, et al.
Published: (2026)

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
by: Mayeux, Arnaud, et al.
Published: (2025)

A complete formalization of Fermat's Last Theorem for regular primes in Lean
by: Best, Alex, et al.
Published: (2024)

Hologram Reasoning for Solving Algebra Problems with Geometry Diagrams
by: Huang, Litian, et al.
Published: (2024)

Formal Verification of the Empty Hexagon Number
by: Subercaseaux, Bernardo, et al.
Published: (2024)

Differential Geometry of Weightings
by: Loizides, Yiannis, et al.
Published: (2020)

Proceedings 14th International Conference on Automated Deduction in Geometry
by: Quaresma, Pedro, et al.
Published: (2024)

On smoothness, tangent cones, and the metric geometry of definable sets
by: Rocha, André Gadelha, et al.
Published: (2025)

Advances in Discrete Differential Geometry
by: Bobenko, Alexander I.
Published: (2018)

Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems
by: Simmons, William, et al.
Published: (2023)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

k-Planar and Fan-Crossing Drawings and Transductions of Embeddable Graphs
by: Hliněný, Petr, et al.
Published: (2025)

Happy Ending: An Empty Hexagon in Every Set of 30 Points
by: Heule, Marijn J. H., et al.
Published: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Differential Geometry
by: Pinkall, Ulrich, et al.
Published: (2024)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
by: Santos, Marco Dos, et al.
Published: (2025)

Intuitionistic Propositional Logic in Lean
by: Trufaş, Dafina
Published: (2024)

Devil's Games and $\text{Q}\mathbb{R}$: Continuous Games complete for the First-Order Theory of the Reals
by: Meijer, Lucas, et al.
Published: (2025)

Completeness Theorems for k-SUM and Geometric Friends: Deciding Fragments of Integer Linear Arithmetic
by: Gokaj, Geri, et al.
Published: (2025)

Computing Diffusion Geometry
by: Jones, Iolo, et al.
Published: (2026)

Hypercovers in Differential Geometry
by: Glass, Cheyne, et al.
Published: (2026)

Lean on Vampire Proofs (Short Paper)
by: Bodingbauer, Jonas, et al.
Published: (2026)

Integral Curves and Flows on Banach Manifolds in Lean
by: Yin, Weichen Winston, et al.
Published: (2026)

Evolving Surfaces and Evolving Implicit Differential Equations Via Contact Geometry and Singularities
by: Uribe-Vargas, Ricardo
Published: (2020)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
by: Moreira, Walter, et al.
Published: (2026)

LeanArchitect: Automating Blueprint Generation for Humans and AI
by: Zhu, Thomas, et al.
Published: (2026)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
by: Pertseva, Elizaveta, et al.
Published: (2026)

ZFLean: a framework for set-level mathematics in Lean
by: Trélat, Vincent
Published: (2026)

Differential Geometry of Synthetic Schemes
by: Cherubini, Felix, et al.
Published: (2025)

Differential Geometry on Pointwise Affine Spaces
by: Jonsson, Dan
Published: (2025)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
by: Yang, Bowen, et al.
Published: (2026)

Structural Validation Of Synthetic Power Distribution Networks Using The Multiscale Flat Norm
by: Lyman, Kostiantyn, et al.
Published: (2024)

Revisiting Anisotropy in Language Transformers: The Geometry of Learning Dynamics
by: Bernas, Raphael, et al.
Published: (2026)

Categorical Foundations of Formalized Condensed Mathematics
by: Asgeirsson, Dagur, et al.
Published: (2024)

Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
by: Mayeux, Arnaud, et al.
Published: (2026)

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
by: Rowney, Tate, et al.
Published: (2026)

Univalent Foundations of Constructive Algebraic Geometry
by: Zeuner, Max
Published: (2024)