a chain of custody for papers in arxiv to formal proofs in Lean

Papers published in arxiv using Latex contain narrative text and mathematical expressions. How could we have confidence that the content of a published paper is related to a formal proof?

The narrative text would refer to symbols, expressions, units, and quantities. The expressions and symbols could be embedded in the Latex source using a package that provides macros.

The author's .tex would include loading a package like

\usepackage{pdg}[server_address=http://serveraddressforpdg.net]

Then when the author references an expression they would use

\begin{equation}
\pdgexp{192839}
\end{equation}

When compiled to PDF, the macro \pdgexp calls to the server address http://serveraddressforpdg.net to return the Latex expression. The same could be done for an inline reference to a symbol, like \pdgsymbol{93831911}. 

In this approach there wouldn't need to be an appendix for the derivation because the derivation steps are hosted on the PDG server.

The chain of custody would be

arxiv PDF -- arxiv .tex -- .tex contains references to PDG expression and symbol IDs -- PDG server contains derivation steps -- steps are validated using Lean

The macro might need to cache the PDG database locally so the server doesn't get called every time the .tex is compiled PDF. 
Also, allow the author to force a refresh of the cache.