🖥️ Computations in Lean (proof of concept for Lean tutorials; incomplete tutorial)

ojs

Author

Kevin Kappelmann

@kappelmann

PhD student interested in interactive theorem proving.

Comments (4)

Job van der Zwan

Jan 10, 2022

I'm getting an error on line 14: unknown identifier 'nat.prime'

Kevin Kappelmann

Jan 10, 2022

Thanks! I fixed it along with other things that broke due to updates in mathlib.

Fabian Iwand

Jan 11, 2022

This empty pinned cell was probably left in by accident? On mobile it covers part of the following text.

Kevin Kappelmann

Jan 12, 2022

Thanks, I removed it.

ProductAbout Pricing Documentation Release notes Contact us

Open sourceNotebook Kit Plot D3

CommunityExplore Forum Bluesky YouTube X

🖥️ Computations in Lean (proof of concept for Lean tutorials; incomplete tutorial) | Kevin Kappelmann | Observable🖥️ Computations in Lean (proof of concept for Lean tutorials; incomplete tutorial) | Kevin Kappelmann | Observable