Twitter | Pretraživanje | |
bgc
Proof assistants are computer programs for writing and verifying formalized mathematical proofs. What's it like to use one? Explore some Fibonacci sum identities with the browser version of the Lean theorem prover in this notebook!
An Observable notebook by Bryan Gin-ge Chen.
Reply Retweet Označi sa "sviđa mi se" More
bgc 29. srp
Odgovor korisniku/ci @blockspins
Part 2 features some very simple "Lean"-driven graphics and shows formalizations of two counting problems where the Fibonacci numbers appear:
Reply Retweet Označi sa "sviđa mi se"
bgc 29. srp
Odgovor korisniku/ci @blockspins
These notebooks use some code gluing Lean & CodeMirror to Observable that I hope you'll try using too! The documentation is here:
Reply Retweet Označi sa "sviđa mi se"
bgc 31. srp
Odgovor korisniku/ci @blockspins
Now you can connect these notebooks to Lean on your computer using "websocketd":
Reply Retweet Označi sa "sviđa mi se"