5 papers
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…
A sign-reversing involution for the antipode of Schur functions
Younggwang Cho, Byung-Hak Hwang, Hojoon Lee
We resolve a question posed by Benedetti and Sagan by constructing a signreversing involution on Takeuchi's expansion that yields the antipode for the ring of symmetric functions i…
Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
Martin Dvorak, Tristan Figueroa-Reid, Rida Hamadani +8
Seymour's decomposition theorem is a hallmark result in matroid theory presenting a structural characterization of the class of regular matroids. Formalization of matroid theory fa…
Refined canonical stable Grothendieck polynomials and their duals, Part 2
Byung-Hak Hwang, Jihyeug Jang, Jang Soo Kim +2
This paper is the sequel of the paper under the same title with part 1, where we introduced refined canonical stable Grothendieck polynomials and their duals with two families of i…
Refinement of Hikita's -positivity theorem via Abreu--Nigro's -functions and restricted modular law
JiSun Huh, Byung-Hak Hwang, Donghyun Kim +2
We study the symmetric functions \( g_{\mm,k}(x;q) \), introduced by Abreu and Nigro for a Hessenberg function \( \mm \) and a positive integer \( k \), which refine the chromatic…