Image de couverture de livre

Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteur principal:	Dvorak, Martin
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science History and Overview
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Ablation and the Meno: Tools for Empirical Metamathematics
par: Fan, Zhengqin, et autres
Publié: (2026)

The paradoxes and the infinite dazzled ancient mathematics and continue to do so today
par: Kamareddine, Fairouz, et autres
Publié: (2024)

Mathematical Proof Between Generations
par: Bayer, Jonas, et autres
Publié: (2022)

Notes on Category Theory with examples from basic mathematics
par: Perrone, Paolo
Publié: (2019)

On a form of intrinsic optimism in Set Theory
par: Pérez, M. Muñoz
Publié: (2025)

In Memory of Martin Davis
par: Calvert, Wesley, et autres
Publié: (2024)

Cantor's Powerset Theorem, Graph-Theoretically
par: Salehi, Saeed
Publié: (2026)

A correspondence problem for mathematical proof
par: DeDeo, Simon, et autres
Publié: (2026)

A definição de verdade de Tarski
par: Cardoso, Guilherme, et autres
Publié: (2024)

From real analysis to the sorites paradox via Reverse Mathematics
par: Dean, Walter, et autres
Publié: (2025)

In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl
par: Neuwirth, Stefan, et autres
Publié: (2024)

Weyl's Quantifiers
par: Toader, Iulian D.
Publié: (2024)

Analytic proofs for logics of evidence and truth
par: Carnielli, Walter, et autres
Publié: (2024)

Automated Mathematics and the Reconfiguration of Proof and Labor
par: Ochigame, Rodrigo
Publié: (2023)

Secrets and Quantifiers
par: Bajnok, Bela, et autres
Publié: (2024)

One Plus One Equals Two Ones: On Identity, Aggregation, and Counting
par: Ghosh, Souvik
Publié: (2025)

On Godel's treatment of the undecidable in 1931
par: Cattabriga, Paola
Publié: (2024)

Guises and Perspectives: An Intentional and Hyperintensional Sketch
par: Colomina-Alminana, Juan J.
Publié: (2026)

Artificial Intelligence and the Structure of Mathematics
par: Barkeshli, Maissam, et autres
Publié: (2026)

Very basic set theory
par: Homan, Doeko
Publié: (2023)

In between myth and reality: AI for math -- a case study in category theory
par: Diaconescu, Răzvan
Publié: (2025)

Anatomy of a Formal Proof
par: Avigad, Jeremy, et autres
Publié: (2024)

The Beauty of Roots
par: Baez, John C.
Publié: (2023)

Operators in the mind: Jan Lukasiewicz and Polish notation
par: Mizraji, Eduardo
Publié: (2025)

Teaching "Foundations of Mathematics" with the Lean Theorem Prover
par: Bottoni, Mattia Luciano, et autres
Publié: (2025)

Revisiting the Sleeping Beauty problem
par: Piva, Paulo S., et autres
Publié: (2024)

Demonstração Formal de um Algoritmo Alternativo da Multiplicação em Base 10
par: Dias, Albert Lucas Lima, et autres
Publié: (2025)

Nelson's Logical Diagrams
par: Aberdein, Andrew
Publié: (2023)

The Reconstruction of Theaetetus' Theory of Ratios of Magnitudes
par: Negrepontis, Stelios, et autres
Publié: (2025)

Elements of the Theory of Probability and Mathematical Statistics
par: Chinarova, Lidiia L., et autres
Publié: (2024)

Countable real analysis
par: Klazar, Martin
Publié: (2023)

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
par: Dvorak, Martin, et autres
Publié: (2025)

Johann Heinrich Lambert's memoir "Theorie der Parallellinien": A review with commentary
par: Papadopoulos, Athanase, et autres
Publié: (2026)

Exploring Gender Differences in Tertiary Mathematics-Intensive Fields: A Critical Review of Social Cognitive Career Theory
par: Gao, Huayu, et autres
Publié: (2025)

Comportamientos extraños del infinito: Gráficas Infinitas
par: Fernández-Bretón, David J., et autres
Publié: (2025)

Rigidity of Graphs and Frameworks: A Matroid Theoretic Approach
par: Cruickshank, James, et autres
Publié: (2025)

The {\em 4DLO} and other tubing models of $S^3$ symmetry
par: Goodman-Strauss, Chaim, et autres
Publié: (2026)

Open Mathematical Tasks as a Didactic Response to Generative Artificial Intelligence in Post-AI Contexts
par: Serrano, Felix De la Cruz
Publié: (2026)

Waterproof Editor: an educational environment for proof assistants and programming languages
par: Otte, Pim, et autres
Publié: (2026)

Controlling Equational Reasoning in Large Language Models with Prompt Interventions
par: Meadows, Jordan, et autres
Publié: (2023)