architectural-blueprint@2x
research

Lean blueprint projects

Leave a comment
Lean is a popular proof assistant. Blueprint projects document Lean projects with Mathlib-style documentation and LaTeX/PDF support. Here are my Lean blueprint projects:
  • Marginis – formalia marginalia for the Journal of Logic and Analysis
  • Protein folding – formalizations related to the paper Nonmonotonicity of protein folding under concatenation
  • Automatic complexity – formalized exercise solutions for my book
  • Dyadic deontic logic – formalized results from a paper in preparation (with Rachelle Edwards)
  • Jaccard – formalization research paper Interpolating between the Jaccard distance and an analogue of the normalized information distance (Journal of Logic and Computation, 2022)

Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>