Jaeseong Heo | Searcharxiv

arXiv2026

Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

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 pipeline consisting of PDF-to-LaTeX preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence. While the preprocessing and autoformalization stages can be largely automated, we find that verification remains the most subtle and labor-intensive component, requiring careful human oversight. Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process. We also compare the performance of different autoformalization models and highlight key bottlenecks in translating informal statements into formal language.

cs.LO↗

arXiv2019

Dirichlet forms and ultrametric Cantor sets associated to higher-rank graphs

The aim of this paper is to study the heat kernel and jump kernel of the Dirichlet form associated to ultrametric Cantor sets $\partial\BB_Λ$ that is the infinite path space of the stationary $k$-Bratteli diagram $\BB_Λ$, where $Λ$ is a finite strongly connected $k$-graph. The Dirichlet form which we are interested in is induced by an even spectral triple $(C_{\operatorname{Lip}}(\PB_Λ), π_ϕ, \mathcal{H}, D, Γ)$ and is given by \[ Q_s(f,g)=\frac{1}{2} \int_Ξ \operatorname{Tr}\big(\vert D\vert^{-s} [D,π_ϕ(f)]^{\ast} [D,π_ϕ(g)] \big) \, dν(ϕ), \] where $Ξ$ is the space of choice functions on $\partial \BB_Λ\times \partial \BB_Λ$. There are two ultrametrics, $d^{(s)}$ and $d_{w_δ}$, on $\partial \BB_Λ$ which make the infinite path space $\PB_Λ$ an ultrametric Cantor set. The former $d^{(s)}$ is associated to the eigenvalues of Laplace-Beltrami operator $Δ_s$ associated to $Q_s$, and the latter $d_{w_δ}$ is associated to a weight function $w_δ$ on $\BB_Λ$, where $δ\in (0,1)$. We show that the Perron-Frobenius measure $μ$ on $\partial \BB_Λ$ has the volume doubling property with respect to both $d^{(s)}$ and $d_{w_δ}$ and we study the asymptotic behaviors of the heat kernel associated to $Q_s$. Moreover, we show that the Dirichlet form $Q_s$ coincides with a Dirichlet form $\mathcal{Q}_{J_s, μ}$ which is associated to a jump kernel $J_s$ and the measure $μ$ on $\partial \BB_Λ$, and we investigate the asymptotic behavior and moments of displacements of the process.

math.PR↗