Steiner's Line Theorem in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Ruy Jose Guerra Barretto de Queiroz
E-Mails 📧
Entries
2026
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Földes–Hammer Characterization of Split Graphs
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Strong Normalization for Church-Style System F
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Napoleon's Theorem
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Steiner Deltoid as the Tangent Envelope of Wallace--Simson Lines in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Miquel's Theorem in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Wallace--Simson Line Theorem in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
General Weierstrass Equations
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Formal Verification of an Explicit Counterexample to the Jacobian Conjecture
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Checking Equality-Saturation Merge and Extraction Certificates
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Chevalley-Warning Theorem
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Fundamental Group of the Circle
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Conway's Circle Theorem in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Correctness and Complexity of BMSSP in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Vosper's Theorem and the Cauchy–Davenport Theorem via the Polynomial Method
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Freiman's 3k - 4 Theorem
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Busy Beaver Function
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
A Reusable Isabelle/HOL Framework for Propositional Labelled Natural Deduction
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Mostowski Collapse Theorem
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Andrew's Monotone Chain Convex Hull Algorithm
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Alon’s Combinatorial Nullstellensatz
by Arthur Freitas Ramos, Ruy Jose Guerra Barretto de Queiroz and David Barros Hulak
The Classical Seifert–van Kampen Theorem
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Erdos-Ginzburg-Ziv
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Nash Equilibria for Finite Games in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Banach–Tarski Paradox in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Aho-Corasick String Matching
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Nagata Factoriality
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz