Numerals are represented in binary?

Stream: new members

[Kevin Cheung]

In Mathematics in Lean section 5.2, there is this sentence: "(Numerals are translated to binary representations, but we don’t have to worry about the details of that now.)"

Does that mean that 3:Nat is actually not Nat.succ (Nat.succ (Nat.succ Nat.zero)) but something else?

[Kyle Miller]

3 is equal to Nat.succ (Nat.succ (Nat.succ Nat.zero)), but the kernel is able to represent this expression internally in a more efficient form (a binary representation), and it also has accelerators for operations such as Nat.add to skip using the recursive definition and instead use a fast add of the binary representation.

[Mark Fischer]

I'm not 100%, but I think this curtails into the trust system too. When you're using Lean to write code instead of proofs, not everything has to go through the kernel, so some extra shortcuts are available. I understand it as wining space/time at the cost of a greater surface area for bugs. I can't find the sources for any of this at the moment though... so grain of salt

[Kevin Cheung]

So how does one write trusted and efficient code in Lean?

[Mark Fischer]

I'm not sure if that question can be answered in the general case yet.

If you want more speed, you'll need to figure out whats slowing you down on a case-by-case basis.

If you want more trust, wait for more verifiers to corroborate on lean's output or even a full-blown formal verification of Lean kernel correctness (then buy trusted formally modeled hardware, etc). If I were writing a math Proof, I wouldn't worry about it. If I'm writing a pace maker where people's lives depend on correctness, maybe an older battle-tested model checker moves the needle forward a bit farther on trust? Definitely I'd do more research before making any such choice.

It may have been lean 3 where you could choose to run computations in a vm or compile to byte-code where the tradeoff between the two is as expected. My search for where I was reading about this has been fruitless, I wish I could point you toward more trusted sources on this as I'm quite fresh to lean and the ecosystem myself.

[Kevin Cheung]

My main concerns at the moment are proofs that involve lots of computations which need to be performed very quickly. I don't think I need pacemaker-level trust but definitely something close to a formal proof.

[Mark Fischer]

My advice is to just give it a go. If you find Lean isn't up to the task for your computationally heavy proof, I don't know how much more performance you could squeeze out of another theorem prover. I imagine it depends heavily on the details of your proof.

If you find a specific thing really bogging you down, posting a #mwe here will likely get friendly experts involved who know all the performance pitfalls and how to work around them.

From a compsci perspective, I've been pleasantly surprised at how well Lean performs. Avoiding monads, my Sudoku Solver is performing admirably close to my Rust implementation. That's not a comprehensive review of performance of course.

[Kevin Cheung]

You have a verified sudoku solver? That's amazing. Is it viewable by the public?

[Mark Fischer]

Still working on it! Writing the Sudoku Solver in Lean was a breeze, verifying it has been my project to direct my learning, so it's been slow-going in the evenings. It'll be viewable by the public eventually.

[Kevin Cheung]

Good luck!

[Kevin Cheung]

I hope I can see it soon.