Is there an existing or planned HTML-to-Verso importer?

Hello,

We are evaluating Verso as the central authoring and publishing system for a
bilingual Greek/English educational project about formal logic and automated
reasoning. Our intended workflow is:

structured HTML -> Verso -> checked interactive HTML + LaTeX/PDF

The input HTML may originate from Mathpix, human editing, or Google Translate.
It can contain headings, paragraphs, lists, tables, footnotes, links, images,
LaTeX/MathML mathematics, and code blocks. Lean examples recovered from the
HTML would subsequently be elaborated and checked by Lean.

We tested the forward directions successfully with Lean 4.34.0-rc1 and Verso
commit aa44714115e9:

Verso -> single-page interactive HTML
Verso -> LaTeX -> PDF

Before implementing the reverse direction, we searched the Verso repository,
documentation, issues, pull requests, and the Lean package ecosystem. We did
not find a documented HTML-to-Verso importer, HTML reader, Pandoc writer, or
round-trip format.

Could you please advise on the following questions?

1. Does an HTML-to-Verso importer or an unpublished prototype already exist?
2. Is such an importer planned or considered within Verso's scope?
3. For an external importer, which target would be preferable and reasonably
   stable: generated Verso concrete syntax, or programmatic construction of
   Verso.Doc / Part Manual values?
4. Would a pipeline based on Pandoc's HTML reader, followed by a Lean 4
   converter into Verso's document model, fit the intended architecture?
5. Does Verso emit, or plan to emit, a machine-readable document artifact that
   preserves enough semantic information for reliable round trips?
6. In generated interactive HTML, what is the recommended way to distinguish
   original Lean source tokens from derived annotations such as tactic states,
   hover data, links, and search metadata?

Our goal is not byte-for-byte recovery of the original .lean source. We want
to produce a semantically equivalent, readable, maintainable, and compilable
Verso document, while reporting unsupported or lossy conversions explicitly.

If this direction is compatible with the project, we would be interested in
developing and documenting an open-source prototype rather than maintaining a
private ad-hoc converter.

Thank you for your work on Verso and for any architectural guidance.

Start by reviewing the Verso repository, documentation, issues, pull requests, and the tested forward paths from Verso to interactive HTML and LaTeX/PDF. The issue names Lean 4.34.0-rc1 and commit aa44714115e9 but no source files or tests; done would be architectural guidance on importer scope, target representation, round trips, and generated HTML metadata.