4 papers
When Finite Free Curves Split
Baran Hashemi, Jihoon Hyun
We characterize equality in the finite free Stam and entropy-power inequalities, proving that Hermite polynomials are the unique extremizers among simple real-rooted inputs, up to…
Algorithmic Cost in "Exact Real Computation"
Jihoon Hyun, Holger Thies, Martin Ziegler
Turing completeness of a programming language or system characterizes its expressive power; and the strong Church-Turing hypo-/thesis refines such from qualitative to polynomial-ti…
Formalizing Flag Algebras in Lean
Gyeongwon Jeong, Seonghun Park, Jihoon Hyun +2
Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefin…
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
Seewoo Lee, Byung-Hak Hwang, Hyojae Lim +10
We present Lean-GAP (Lean-Graduate Agebra Problems), 430 formalized graduate-level algebra problems from the textbook Abstract Algebra by Dummit and Foote. We develop a scalable pi…