How exactly does Lean Blueprint actually integrate with Lean

Stream: new members

[Noah Stebbins]

Hey guys,

This might be a dumb question but when I first started looking at Lean Blueprint, I assumed it would generate a PDF and a website based solely on my Lean code, but when I look at projects that use Lean Blueprint and when I tried it out myself, it seemed like I needed to provide all of the Latex anyways. For example, it didn't look like /leanok or /lean "injected" anything if that makes sense.

For example, in PFR, the proof is actually written out in Latex.

Am I missing something or am I just not using it properly?

I'm looking for a tool that takes my Lean code as-is and basically generates human readable output without me having to do a lot of boilerplate.

I started a simple project with Blueprint here but I haven't managed to generate the proofs yet.

[Riccardo Brasca]

Do you mean the proofs written in English? Those are 100% written by humans.

[Edward van de Meent]

as i understand it, the intention for Lean Blueprint is working the other way: start out with a LaTeX proof, then make the graph associated with the proof, to then be able to organise the Lean proofs

[Edward van de Meent]

which you also write yourself

[Noah Stebbins]

Gotcha, is there any tool that takes a Lean proof and gives some kind of human readable output? So basically showing how equations and propositions get manipulated with every step

[Michael Rothgang]

Is there a prototype for such a tool, developed by @Patrick Massot and @Kyle Miller. (There used to be a demo on this webpage, which apparently is offline now.)

[Michael Rothgang]

My understanding is that this works well for some examples, but making it ready for broader consumption requires some amount of work which has not been done yet. (Please correct me if I'm wrong!)

[Kevin Buzzard]

There are demos at the bottom of Kyle Miller's home page right now.

[Patrick Massot]

Yes, this is the job of InformalLean, not LeanBlueprint. And the demo on my webpage is still there, Michael’s simply put a random space in the url. The correct url is https://www.imo.universite-paris-saclay.fr/~patrick.massot/Examples/ContinuousFrom.html, which was generated from https://www.imo.universite-paris-saclay.fr/~patrick.massot/Examples/ContinuousFrom.lean (you may need to tell your webbrowser than the Lean file is encoded in utf8).

[Michal Wallace (tangentstorm)]

Patrick Massot said:

(you may need to tell your webbrowser than the Lean file is encoded in utf8).

If your Apache administrators have allowed, you may be able to fix this by adding a file called .htaccess to your web directory with the following line:

AddCharset UTF-8 .lean

Is InformalLean open source and online somewhere?

[Patrick Massot]

I already tried such .htaccess tricks, but they have no effect there.

[Patrick Massot]

InformalLean is not yet public.