boost confidence w/o a proof

Stream: lean4

[Matthew Ballard]

The discussion #lean4 > quickchecks Gen monad led me to a general question. Is there anything that Lean can offer to improve the confidence of a conjecture in absence of a (formal) proof?

I ask this here instead of #general because Lean 4 compiles down to a binary so I can dream I can run numerical tests on a question somewhat robustly.

[Henrik Böving]

Well that'd be tests and its strong type system...although you could argue that in order to actually use said strong type system to its fullest potential you have to write proofs, even if its not direclty about lemmas but "just" about stuff like "this index is within bounds" etc.

[Matthew Ballard]

What kind of tests can I run on the Riemann hypothesis?

[Kevin Buzzard]

you could compute the first million nontrivial zeros

[Matthew Ballard]

Right, is this a reasonable thing for Lean 4 computationally?

[Henrik Böving]

Definre "reasonable"

[Kevin Buzzard]

Well Riemann did the first one by hand

[Matthew Ballard]

Better than doing it Python for example

[Henrik Böving]

Better as in faster?

[Matthew Ballard]

Yes, faster

[Henrik Böving]

I wouldn't dare to say yes without a benchmark on this but I'd guess that due to the fact that Lean is compiled to C vs python being bytecode interpreted it should definitely be able to produce faster code than pure python

You are however most likely talking about python with its funky numerics libraries which all work in C and expose an API to python. Which you could of course do in Lean as well but hasn't been done right now

[Matthew Ballard]

Another analogous question: would it make sense to rewrite say Macaulay2 in Lean 4 to both prove stuff about the math and then compute stuff?

[Matthew Ballard]

I use M2 as an example since it is go-to for commutative algebra testing

[František Silváši]

These questions cannot be answered very simply. You can expect Lean 4 performance (now and even more so in the future) to be comparable wiht performance of other functional languages (native or pseudo-native, so, say, Haskell to native, or 'old Haskell' with Haskell -> C -> native). So the best way to look at it is if you're comfortable with standard Haskell-like performance for your particular problem.

[Matthew Ballard]

It sounds like experimentation is in order then.

[Henrik Böving]

In the end its unlikely Lean will ever be able to consistently keep up with programming languages like C or C++ out of the box. But that is also not the point, it cannot possibly keep up with languages where you have such fine grained control over what is happening while we abstract quite a bit away from memory management etc.

[František Silváši]

The question of performance cannot really be considered in a broad sense beyond some basics a'la Lean is native (not interpreted)

[Matthew Ballard]

Great. I take from this that is reasonable to try it out and see.