https://github.com/chboishabba/agda2lean
Hi! A brief update on agda2lean:
This is now a working path from checked Agda code to Lean-facing output. It is not a text converter: it starts from Agda's checked representation, records declarations and their dependencies in a small shared format, then produces Lean output and checks the result independently.
The immediate goal is modest: make small, well-understood Agda developments usable from Lean while being clear about what translated directly, what needs a Lean-side proof, and what is not supported yet.
We are also thinking about a proof-wiki-style layer: a browsable record for each translated declaration, linking the Agda source, Lean result, dependencies, and the translation receipt. Much of the underlying record-keeping is already part of agda2lean; the wiki would make it useful to people rather than only to the build.
This is related to the aim of Logipedia, which uses Dedukti to make proofs available across systems. We are not putting Dedukti in agda2lean's main translation path. For us, it is a possible later independent audit route; the near-term work remains a practical, checkable Agda-to-Lean path.
I'd especially welcome advice on:
- the kinds of Agda material that would be most useful to bring into the Lean/mathlib world;
- how Lean users would want translated declarations and their provenance presented;
- existing mathlib conventions or projects we should align with.
https://github.com/chboishabba/agda2lean
Hi! A brief update on agda2lean:
This is now a working path from checked Agda code to Lean-facing output. It is not a text converter: it starts from Agda's checked representation, records declarations and their dependencies in a small shared format, then produces Lean output and checks the result independently.
The immediate goal is modest: make small, well-understood Agda developments usable from Lean while being clear about what translated directly, what needs a Lean-side proof, and what is not supported yet.
We are also thinking about a proof-wiki-style layer: a browsable record for each translated declaration, linking the Agda source, Lean result, dependencies, and the translation receipt. Much of the underlying record-keeping is already part of agda2lean; the wiki would make it useful to people rather than only to the build.
This is related to the aim of Logipedia, which uses Dedukti to make proofs available across systems. We are not putting Dedukti in agda2lean's main translation path. For us, it is a possible later independent audit route; the near-term work remains a practical, checkable Agda-to-Lean path.
I'd especially welcome advice on: