Zulip Chat Archive

Stream: general

Topic: performance Lean vs Z3

Miguel Raz Guzmán Macedo (Mar 27 2020 at 19:05):

I just saw that Leonardo de Moura was one of the principal architects of both Z3 and Lean. That is awesome! Are there any benchmarks on Z3 vs Lean performance?

Mario Carneiro (Mar 27 2020 at 19:06):

they are not directly comparable

Miguel Raz Guzmán Macedo (Mar 27 2020 at 19:08):

I understand that Z3 is an SMT solver. Does Lean at some point also not contain some sort of solver?

Mario Carneiro (Mar 27 2020 at 19:09):

No

Mario Carneiro (Mar 27 2020 at 19:09):

Lean has a bunch of tactics, some of which may call solvers, but most don't

Kevin Buzzard (Mar 27 2020 at 19:09):

The solver is this chatroom in Lean

Kevin Buzzard (Mar 27 2020 at 19:10):

have you got some spare CPU cycles? We're trying to prove some theorems

Mario Carneiro (Mar 27 2020 at 19:10):

there are some algorithms that may have been borrowed from Z3, for example, cc and eblast, but TBH they aren't used very often

Miguel Raz Guzmán Macedo (Mar 27 2020 at 19:12):

Kevin Buzzard said:

have you got some spare CPU cycles? We're trying to prove some theorems

Anything related to physics ?

Mario Carneiro (Mar 27 2020 at 19:12):

what kind of physics?

Miguel Raz Guzmán Macedo (Mar 27 2020 at 19:13):

Classical mechanics, GR, or PDEs

Mario Carneiro (Mar 27 2020 at 19:16):

I think it would be really cool to see GR foundations in lean. We have stuff on manifolds and "holors" (what physicists call tensors), but I don't think we have anything to do with Riemannian manifolds and geodesics

Miguel Raz Guzmán Macedo (Mar 27 2020 at 19:36):

Well, I've completed the natural number game, and would appreciate unrusting my relativity, so if people know how I could start, I would welcome that.

Miguel Raz Guzmán Macedo (Mar 27 2020 at 19:41):

Or is there anything done on Lagrangian/Hamiltonian formalisms?

Andrew Ashworth (Mar 27 2020 at 19:51):

Here's a paper; maybe it's useful? https://arxiv.org/pdf/1005.0960v2.pdf

Andrew Ashworth (Mar 27 2020 at 19:53):

It's a synthetic development, which may or may not be interesting to you...

Andrew Ashworth (Mar 27 2020 at 19:58):

I found it by searching; it was some Harvard student's senior thesis to formalize this in Coq: https://dash.harvard.edu/handle/1/38811518

Patrick Massot (Mar 27 2020 at 20:01):

Miguel Raz Guzmán Macedo said:

Well, I've completed the natural number game, and would appreciate unrusting my relativity, so if people know how I could start, I would welcome that.

Going from the properties of addition and multiplication of natural numbers to relativity maybe a slightly too big jump....

Miguel Raz Guzmán Macedo (Mar 27 2020 at 20:23):

Andrew Ashworth said:

I found it by searching; it was some Harvard student's senior thesis to formalize this in Coq: https://dash.harvard.edu/handle/1/38811518

Hey, this includes the Coq code he used. Maybe transcribing it into Lean is just manageable. Would you happen to know a similar effort in Coq to prove the Hamiltonian or Lagrangian formalisms?

Miguel Raz Guzmán Macedo (Mar 27 2020 at 20:35):

Also, @Kevin Buzzard what's the big difference between the performance of proof vs tactic mode in Lean? Does a succesful tactic proof get compiled down to a term proof?

Mario Carneiro (Mar 27 2020 at 20:45):

Yes, you can use #print to see the resulting term

Mario Carneiro (Mar 27 2020 at 20:46):

Tactic mode is usually slower than term mode, as tactics have to construct the term. You may be surprised to find that it's not always slower, because term mode also has automation behind it, namely elaboration, and this can also be significantly expensive in some cases.

Mario Carneiro (Mar 27 2020 at 20:47):

However you have to ask yourself if the speed gain is worth it. Don't get caught in the micro-optimization trap

Mario Carneiro (Mar 27 2020 at 20:48):

(says the guy who decided to write his own theorem prover because lean was too slow)

Miguel Raz Guzmán Macedo (Mar 27 2020 at 21:10):

Ha, thanks Mario! You would know if anyone has reimplemented the Lean kernel in Rust right?

Andrew Ashworth (Mar 27 2020 at 21:12):

I don't think anybody has done that

Andrew Ashworth (Mar 27 2020 at 21:14):

Step 1: be familiar with the calculus of inductive constructions. Step 2: be familiar with the implementation of functional programming language compilers. Step 3: draw the owl in Rust

Mario Carneiro (Mar 27 2020 at 21:16):

Actually it has been done, see nanoda

Andrew Ashworth (Mar 27 2020 at 21:16):

But you never know. Somebody here a few weeks ago wanted to implement the Lean kernel on an FPGA

Andrew Ashworth (Mar 27 2020 at 21:16):

is that the kernel or just a type-checker?

Mario Carneiro (Mar 27 2020 at 21:16):

what's the difference?

Andrew Ashworth (Mar 27 2020 at 21:18):

Does elaboration, unification, type-class inference not count as part of the kernel? ¯\_(ツ)_/¯

Mario Carneiro (Mar 27 2020 at 21:19):

I would consider none of that part of the kernel

Mario Carneiro (Mar 27 2020 at 21:19):

I suppose you could call it part of the type checker front end

Andrew Ashworth (Mar 27 2020 at 21:19):

I guess my definition is wrong. Is there a type-checker for that?

Mario Carneiro (Mar 27 2020 at 21:20):

To me type checker and kernel are mostly synonymous. There are no implementations of the lean front end other than lean

Mario Carneiro (Mar 27 2020 at 21:20):

(which I consider to be a serious trustworthiness hole)

Mario Carneiro (Mar 27 2020 at 21:21):

but it's hard to do otherwise because lean is so complicated

Mario Carneiro (Mar 27 2020 at 21:21):

the reason lean is slow has little to do with the implementation and everything to do with what it is being asked to do

Mario Carneiro (Mar 27 2020 at 21:22):

If you ever try tracing anything you will realize that lean is doing a phenomenal amount of work

Mario Carneiro (Mar 27 2020 at 21:23):

For typeclass inference in particular I am amazed that lean is able to perform as well as it does considering how much it has to churn through

Miguel Raz Guzmán Macedo (Mar 27 2020 at 21:57):

Andrew Ashworth said:

It's a synthetic development, which may or may not be interesting to you...

Sorry, what does synthetic mean here?

Mario Carneiro (Mar 27 2020 at 22:01):

It means that the treatment is syntactic, using axioms for basic rules about relativity etc. rather than defining things as you would in regular mathematics, using e.g. functions on an infinite dimensional complex vector space

Mario Carneiro (Mar 27 2020 at 22:02):

wait, I got confused whether we are talking about general relativity or quantum mechanics. Well, the point is the same

Miguel Raz Guzmán Macedo (Mar 27 2020 at 22:05):

Ah, works for me! Thanks Mario.

Kevin Buzzard (Mar 27 2020 at 22:05):

You'd better not do both in Lean because they contradict each other, right?

Mario Carneiro (Mar 27 2020 at 22:05):

No, the relation is akin to models of a formal theory

Miguel Raz Guzmán Macedo (Mar 27 2020 at 22:06):

I guess that would be more of a reason to try and formalize it - see what breaks up.

Mario Carneiro (Mar 27 2020 at 22:06):

you should be able to prove that the "semantic" version is an instance of the axioms of the "syntactic" version

Mario Carneiro (Mar 27 2020 at 22:07):

You only get into trouble if you start making ontological claims like "nothing exists except for points that are described by the syntactic theory" therefore your models are necessarily countable

Mario Carneiro (Mar 27 2020 at 22:10):

So in some respects, the syntactic / synthetic approach is more general, but the semantic approach has the advantage that you can prove facts by reference to the model itself, there is no constraint on how you conduct a proof

Patrick Massot (Mar 28 2020 at 11:29):

I think Kevin meant "general relativity and quantum mechanics contradict each other", not "synthetic vs semantic".

Mario Carneiro (Mar 28 2020 at 11:34):

Ah, I missed that. Although it would be pretty tricky to actually derive a contradiction since they are so incompatible

Mario Carneiro (Mar 28 2020 at 11:35):

it would be like proving that the unit circle is disjoint from a lemon

Patrick Massot (Mar 28 2020 at 11:43):

it would be like proving that the unit circle is disjoint from a lemon

I saw this message popping up as an out of context desktop notification, it was pretty weird (and I didn't guess it was answering one of my messages).

Kevin Buzzard (Mar 28 2020 at 12:06):

I think that's undecidable in Lean

Last updated: Dec 20 2023 at 11:08 UTC