Nagata Factoriality. - Arthur Freitas Ramos; David B. Hulak; Ruy José Guerra Barretto de Queiroz (Arch. Formal Proofs, 2026)

Aho-Corasick String Matching. - Arthur Freitas Ramos; David B. Hulak; Ruy José Guerra Barretto de Queiroz (Arch. Formal Proofs, 2026)

The Banach-Tarski Paradox in Isabelle/HOL. - Arthur Freitas Ramos; David B. Hulak; Ruy José Guerra Barretto de Queiroz (Arch. Formal Proofs, 2026)

Nash Equilibria for Finite Games in Isabelle/HOL. - Arthur Freitas Ramos; David B. Hulak; Ruy José Guerra Barretto de Queiroz (Arch. Formal Proofs, 2026)

Andrew's Monotone Chain Convex Hull Algorithm. - Arthur Freitas Ramos; David B. Hulak; Ruy José Guerra Barretto de Queiroz (Arch. Formal Proofs, 2026)

The Mostowski Collapse Theorem. - Arthur Freitas Ramos; David B. Hulak; Ruy José Guerra Barretto de Queiroz (Arch. Formal Proofs, 2026)

Alon's Combinatorial Nullstellensatz. - Arthur Freitas Ramos; Ruy José Guerra Barretto de Queiroz; David B. Hulak (Arch. Formal Proofs, 2026)

Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions. - David B. Hulak; Arthur F. Ramos; Ruy J. G. B. de Queiroz (CoRR, 2026)

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0. - David B. Hulak; Arthur F. Ramos; Ruy J. G. B. de Queiroz (CoRR, 2026)

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL. - David B. Hulak; Arthur F. Ramos; Ruy J. G. B. de Queiroz (CoRR, 2026)