starting Lean and Lean version

Stream: new members

[Martin Harrison]

Hi,

I am new to Lean but not to formal methods. I am working on a library for reasoning about artificial neural networks. Should I be using Lean3? Should I use Lean4? Should I use both in parallel? If I want to maintain and use 3 and 4 on the same system, what is the cleanest way to do that on an Ubuntu machine?

Someone, please advise me on the most sensible way to use Lean given that my goal is to publish a Lean library that I hope will be used by others.

Thanks for your attention,

Martin

[Alistair Tucker]

Will the library contain a working implementation?

[Martin Harrison]

Alistair Tucker said:

Will the library contain a working implementation?

What is a "working implementation"?

[Alistair Tucker]

I suspect the answer to your question is Lean 3. If you wanted to begin by programming a working implementation of an ANN, perhaps one could make a case for Lean 4.

[Martin Harrison]

I want to start by reading in an ONNX file and parsing it, creating the objects defined therein. I need to be able to evaluate on an input the model defined in the ONNX file, but also to prove things about general input-output relations of the model.

What is it exactly that might make the case for Lean 4? Trying to understand - thanks!

[Alistair Tucker]

So Lean 4 is going to be great for doing things like reading files, manipulating IEEE Floats and interfacing with external libraries. (Disclaimer: I haven't done any of those things myself.) When it comes to proving things about your programs I can think of a couple of issues you face. The first is that Floats aren't Reals. The Reals are noncomputable but have all the nice theoretical properties and a wealth of facts about them in the community library mathlib. You may want to resolve this issue by making your functions polymorphic; your proofs will apply to the Real version but you can use the Float version to get numbers out. The second issue is that mathlib doesn't yet work with Lean 4. That situation should be changing soon-ish (within months).

[Martin Harrison]

Great, that makes sense, plus you addressed my very next question! It will be important to prove things about behavior on actual Float values. That is frustrating but encouraging news about mathlib - where can I track that and is there anything that a beginner can do to hasten it?

Also, is it the case that Lean 3 cannot even read in files or merely that Lean 4 will be better for that sort of thing?

Thanks!

[Martin Harrison]

Martin Harrison said:

Great, that makes sense, plus you addressed my very next question! It will be important to prove things about behavior on actual Float values. That is frustrating but encouraging news about mathlib - where can I track that and is there anything that a beginner can do to hasten it?

Also, is it the case that Lean 3 cannot even read in files or merely that Lean 4 will be better for that sort of thing?

Thanks!

Surely some subset of the established results pertaining to Reals also apply to Float? Is it precious few? None at all? I appreciate the difference, but where can I take stock of what is available?

I am looking here for starters - is this the basis for Real?

[Yaël Dillies]

We now have docs#interval and I am currently writing the arithmetic operations on them

[Yaël Dillies]

Then we can define dyadic numbers in a computationally nice way.

[Martin Harrison]

Thanks @Yaël Dillies
Do you know anything about reading in files? Like, could I read in a JSON and parse it with existing tools or would that take a lot of extra work?

[Yaël Dillies]

That I have no idea! I am only interested in floats because they are an application of intervals!

[Arfur Schloppenhowler]

I appreciate your candor.

[Johan Commelin]

@Martin Harrison This might help: https://agentultra.github.io/lean-4-hackers/

[Arfur Schloppenhowler]

Johan Commelin said:

Martin Harrison This might help: https://agentultra.github.io/lean-4-hackers/

Killer, thanks!

[Eric Wieser]

Reading json with lean 3 is very possible, we have docs#json.parse and likely something in the io namespace to read files

[Kevin Buzzard]

There are no problems maintaining and using both lean 3 and 4 on an Ubuntu machine, I have this setup and it just works out of the box. For me the big difference between lean 3 and lean 4 is: do you want access to a million lines of lemmas in pure mathematics?

[Jason Rute]

Arfur Schloppenhowler said:

I am working on a library for reasoning about artificial neural networks.

I would also point you to FormalML. It is in Coq and not Lean, but it might provide some inspiration or collaboration opportunities.

[Arfur Schloppenhowler]

Jason Rute said:

Arfur Schloppenhowler said:

I am working on a library for reasoning about artificial neural networks.

I would also point you to FormalML. It is in Coq and not Lean, but it might provide some inspiration or collaboration opportunities.

Thanks, this is much appreciated! :meat: :cut_of_meat:

I have used Coq but did not know about that project and will definitely try it out.

[Alistair Tucker]

@Arfur Schloppenhowler There is also Certigrad, but it looks like it hasn't been touched in quite a while.

[Alistair Tucker]

@Daniel Selsam Does Certigrad have a future?

[Arfur Schloppenhowler]

Interesting approach to a different problem, almost certainly will help to study it. Thank you, bonus meats for keeping it Lean-based :meat::meat::meat:

[Tomas Skrivan]

I'm working on SciLean which is partially inspired by Certigrad. However, my main focus is on usability then performance and only then on verification. So it might be useful only as an inspiration.

[Arfur Schloppenhowler]

@Tomas Skrivan Very cool! Do you read in any data from disk with SciLean?

[Tomas Skrivan]

No, so far I didn't read any data from files.