Ender

Stream: new members

[Ender]

Hi, I am new to Lean!

I am interested in, for my Master's thesis, either designing a very lightweight Lean GUI or making my own proof assistant from scratch, which is why I ask: If I wanted to learn about the theory behind proof assistants where would I start?

[Kenny Lau]

Ender said:

Hi, I am new to Lean!

I am interested in, for my Master's thesis, either designing a very lightweight Lean GUI or making my own proof assistant from scratch, which is why I ask: If I wanted to learn about the theory behind proof assistants where would I start?

Welcome! You might want to check out The Type Theory of Lean by Mario Carneiro.

[Niels Voss]

Hi, I recommend that if you want to learn the basic type theory that makes Lean work, that you check out #tpil. If instead you want to learn the metamathematics that lean is built upon, then you can check out The Type Theory of Lean, as Kenny Lau mentioned. There's also the book Type Checking in Lean 4 (https://ammkrn.github.io/type_checking_in_lean4/) which gives a description of how the typechecker works.

I'm not sure what you mean by making a GUI for Lean, but depending on what you want to do, you can check out the proofwidgets system, which lets you make any sort of react or html+javascript object in Lean's infoview that can interact with Lean code. An example would be a rubik's cube where if you rotate it, it modifies your code. Lean's metaprogramming features are quite powerful, so if you have a specific idea in mind you might want to mention it here so that people can give you guidance as to what tools you can use to save time.

[Tanner Duve]

I wrote a toy proof assistant that drew aspects from Lean and Coq. I used type theory of lean as a reference as well as this Coq documentation

[Martin Dvořák]

Hi! I'd love to have a lightweight GUI library for Lean!