4 papers
From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4
Daniel Goldberg, Antoine Vinciguerra
We formalize the Dirichlet integral and several of its classical applications in the Lean~4 proof assistant. Since the sinc function is not Lebesgue integrable on the positive half…
A Formalization of the Laplace Transform and Its Inversion in Lean 4
Daniel Goldberg, Antoine Vinciguerra
We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem proved through rea…
Linear Matroid Intersection is in Catalytic Logspace
Aryan Agarwala, Yaroslav Alekseev, Antoine Vinciguerra
Linear matroid intersection is an important problem in combinatorial optimization. Given two linear matroids over the same ground set, the linear matroid intersection problem asks…
Catalytic Computing and Register Programs Beyond Log-Depth
Yaroslav Alekseev, Yuval Filmus, Ian Mertz +2
In a seminal work, Buhrman et al. (STOC 2014) defined the class of problems solvable in space with an additional catalytic tape of size , which is a tape whose…