34 citations · 39 across the 12 of their papers we have counts for
4 papers · 1 filter
Reformalization of the Jordan Curve Theorem
Simon Guilloud, Sankalp Gambhir, Samuel Chassot
We present a case study in reformalization, a variant of autoformalization in which the input proof is not natural language but a formal development in a different proof assistant.…
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Lazar Milikic, Simon Guilloud, Khanh Nguyen +1
We present and evaluate LeanFlow, an LLM agent system specialized for translating mathematical papers into buildable Lean projects. Recent verifier-in-the-loop systems show that la…
Orthologic for SAT Solving
Vladislas de Haldat, Simon Guilloud, Viktor Kunčak
We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementati…
Are Dependent Types in Set Theory Feasible?
Yunsong Yang, Simon Guilloud, Viktor Kunčak
Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, wi…