new to lean

Stream: new members

[Bill Cochran]

hi! i'm new to lean. i did some rust in a past life, so that's helping a bunch. i'm working on a book, more of a passion project than anything right now. the math is really complex, lots of indices and tags. so i was looking to use lean to make sure i have done it right. i have written my first theorem (!) that appears to compile (!!). i have a repo here: https://github.com/wkcochran123/measurement/tree/development

well, at least i think i have written my first theorem in lean. my experience from rust suggests that it works as implemented. is that all there is?

[Vlad]

It may be better to use a class instead of axioms:

class Entropy where
  Instrument : Type u
  Symbol : Instrument → Type v
  symbolFintype : (i : Instrument) → Fintype (Symbol i)
  -- ...

[Eric Wieser]

Could you link to the relevant file, and perhaps delete all the "hello world" files?

[Bill Cochran]

https://github.com/wkcochran123/measurement/blob/development/lean/Entropy/Chapter2/Propositions.lean

[Bill Cochran]

This is the proposition

[Bill Cochran]

the thing that needs instantiation is the instrument, not entropy

[Bill Cochran]

that's the thing i am leaving out

[Bill Cochran]

i want to see if i can instantiate it.

[Bill Cochran]

e.g. set of instruments > 0

[Bill Cochran]

or, my guess set of instruments > 3

[Eric Wieser]

If you want to instantiate, you should replace your axioms with variables

[Bill Cochran]

no, i need to specify the interface
not the data.

[Bill Cochran]

the data need not be known.

[Eric Wieser]

variable means "this is not known right now, but something downstream can specify it"

[Bill Cochran]

nothing can specify it

[Eric Wieser]

axiom means (among other things) "this can never be known / instantiated"

[Bill Cochran]

it need not ever be known

[Bill Cochran]

correct

[Bill Cochran]

that's the thing i want to instantiate an instrument from

[Eric Wieser]

axiom Instrument : Type u prevents you from saying "there are three instruments" by setting Instrument := Fin 3

[Bill Cochran]

i know

[Eric Wieser]

But is that not exactly what you asked to do?

[Bill Cochran]

i have to prove the set of instruments >= k

[Bill Cochran]

thats why instrument is an Nat

[Bill Cochran]

and is assumed to exist.

[Bill Cochran]

this is using a lot of my rust skills to guess at

[Bill Cochran]

but the way rust interprets the memory is how the proof works.

[Bill Cochran]

so far

[Bill Cochran]

so, the theorem is true. if it compiles, correct? these are the unit tests for my book.

[Bill Cochran]

but, i want to say i started going down this path the way you suggested.

[Bill Cochran]

before i figured out this is rust like and not c++ like

[Eric Wieser]

(note that the convention on Zulip tends to be to combine messages into one a bit like you would for an email, rather than a stream of consciousness in the way that discord is used)

[Bill Cochran]

my apologies. i do want to say thank you so much for looking!

[Bill Cochran]

what i am hearing is that the theorem is rather trivial. that is my hope. this is supposed to be straightforward enough to do in ZFC. it gets a lot harder very soon. as long as it building means it passes and i think i have the interfaces correct, then i am go for more testing! thanks for helping. next time i come back i hope it is a much harder challenge for you.

[Eric Wieser]

Your axioms are inconsistent:

example : False :=
  letI : RecordOrder Unit := ⟨fun _ _ => True⟩
  letI : EventOrder Unit := ⟨fun _ _ => True⟩
  ockham_order_coherence (fun _ _ => ()) (e₁ := ()) (e₂ := ()) trivial () trivial

[Eric Wieser]

I strongly recommend not using axiom at all

[Bill Cochran]

instantiable instead of pure interface. i think i can refactor back into that now that i have done it on the interface. i was thinking api -> impl -> exec pattern, but i can just do api -> impl. thanks for your help.

[Eric Wieser]

The way to write an API (assuming you mean an interface) is to use class, not axiom

[Bill Cochran]

i'm talking specifying maps. i need to specify the cardinality of sets in a bunch of different ways.

[Bill Cochran]

this is a cardinality comparison proof.

[Bill Cochran]

taken a very very very very long way.

[Bill Cochran]

turning off now sorry for the spam everyone.

[Eric Wieser]

If you haven't already, take a look at #mwe; if you can reduce questions to this format, you will almost certainly get helpful answers from this channel!

[sujan]

Hi it feels great to be here. Hope I will be able to learn.

[Swapna Iyer]

Hi I am Swapna, building https://app.thelabcompany.co/ so everyone can participate in building cool things with technology. I am new to lean and building with Rust the Agentic AI systems needed for a social network and recommendation systems. With AI in the picture, looking to use proof techniques for verification. If there is any work/libraries used in AI, please do share. Thank you!

[Mateo Bartellini Huapalla]

Hi, I am Mateo Bartellini Huapalla, new to lean and slowly getting to know the formal verification/automated reasoning world. Super thankful to Daniel Dia and the team behind Proof101, excited to follow their seminars!

[Loren Abdulezer]

Hello all, I am Loren Abdulezer, and am new to Lean. Attending the course Proof 101. I am interested in verification and theorem proving in some areas having some applicability in physics.