Buffon's Needle

Stream: general

[Enrico Borba]

I have a (not clean) formalization of both cases of Buffon's Needle, in this file. This is using a "slightly" older version of mathlib.

[Enrico Borba]

I chose to go the formalize the definition of the problem using random variables, just because I thought that definition was closer to the original statement of the problem. This is in contrast to the formalization done in Isabelle, which defines a set and computes its measure.

[Enrico Borba]

If the list is up to date, I think this is the first lean formalization?

[Enrico Borba]

Also, my lean inexperience really shows in the length of this proof

[Johan Commelin]

Congratulations! I think this is indeed the first Lean formalization.

[Johan Commelin]

Are you interested in contributing the more general lemmas in your file to mathlib? The rest of your formalization on Buffon's Needle would make a great contribution to the archive: https://github.com/leanprover-community/mathlib4/tree/master/Archive

[Enrico Borba]

Thanks! I'd definitely be interested in contributing any lemmas you feel are general enough to mathlib, and to the Archive. What's the process for this? Would I open some PRs first for the general lemmas and then modify the formalization so it imports the newly added lemmas?

[Riccardo Brasca]

Yes, this is the normal way to do. You can have a look here for the PR process.

[Riccardo Brasca]

In general try to start with small PRs, you will get quicker reviews.

[Enrico Borba]

Who should be assigned to a PR like this?

[Enrico Borba]

The PR is #10189

[Kyle Miller]

If you add the awaiting-review label (I just did that for you -- usually that's up to an author, but it seemed like you're looking for review!), then if you see "All checks have passed", then it will appear in #queue, which is what reviewers tend to look at. There are also a number of t-* labels for different subjects.

[Enrico Borba]

Sweet, thanks a ton!

[Enrico Borba]

I looked for an 100 theorems label but I didn't see one, same with "archive", so I wasn't sure if there was another label I should use

[Enrico Borba]

Hello, just bumping this thread since the PR remains open. It's been about a month since the last review. Apologies if I should be the one driving this, I'm not super familiar with the customs / etiquette around a PR like this that doesn't really contribute to the stdlib

[Ruben Van de Velde]

I added a few minor comments, but it'd be nice if someone who knows more about probability also took a look

[Enrico Borba]

Thanks for the additional comments

[Enrico Borba]

@Rémy Degenne, pinging you here specifically since I see that you've recently touched a bunch of files under Mathlib/Probability, do you mind taking a look? Or pointing me towards someone else if not?

[Yaël Dillies]

Rémy is very busy right now. I might be able to review, but not right now. Feel free to ask for my review through the Github interface

[Enrico Borba]

Got it, thanks. I'll add you once I merge in master

[Enrico Borba]

@Yaël Dillies thank you for your comments. One last thing about 100.yaml, I added the lines as decls but there are some build errors. I don't think the imports in Archive.lean is visible when checking the declarations in 100.yaml. Let me know if I'm missing something.

[Yaël Dillies]

@Patrick Massot, am I right to think that you were the one setting up the yaml file check? Can we make sure that the yaml files can refer access to archive declarations?

[Patrick Massot]

I don’t think I did that. I may have done the analogue check for the undergrad and overview files. But that would have been in 2020 so I wouldn’t really know more than you when looking at the code.

[Yaël Dillies]

I want to say "Damn, you're old" but actually I started using Lean in 2021 so I am old too :rolling_on_the_floor_laughing:

[Yaël Dillies]

Okay, I assume it's just a matter of adding some Archive.lean file and importing it in the right spot

[Patrick Massot]

Actually, thinking about it, this has to have been redone for Lean 4 and I’m more confident I wasn’t involved.

[Enrico Borba]

I think all that needs to be done is in checkYaml.lean, we need to add a reference to Archive in:

unsafe def main : IO Unit := do
  CoreM.withImportModules #[`Mathlib, `Archive] -- added `Archive here
      (searchPath := compile_time_search_path%) (trustLevel := 1024) do
    let decls := (←getEnv).constants
    let results ← databases.mapM (fun p => processDb decls p)
    if results.any id then
      IO.Process.exit 1

[Enrico Borba]

Testing this out in my branch now, I think it works as it passes the 100.yaml build step

[Enrico Borba]

Indeed, checks pass: https://github.com/leanprover-community/mathlib4/pull/10189

[Yaël Dillies]

I opened #11562 for the change to CI

[Enrico Borba]

I don't have merge permissions, but it looks like everything is ready to go?

[Eric Wieser]

I've sent #10189 to bors (with delegation for some style nits); I can't comment on whether the approach is mathematically clean, but certainly the Lean code looks unusually structured

[Enrico Borba]

Any general comments on how to make the code more "usually" structured. Or any token examples of well-structured code that I can reference?

[David Loeffler]

I think Eric meant that your code is unusually well-structured, not that it is structured in an unusual manner :smile:

[Enrico Borba]

David Loeffler said:

I think Eric meant that your code is unusually well-structured, not that it is structured in an unusual manner :smile:

Hope so! :)

[Ruben Van de Velde]

Yeah, in an unusual manner [positive]

[Ruben Van de Velde]

And thanks for your patience

[Enrico Borba]

Ruben Van de Velde said:

And thanks for your patience

Likewise!

[Enrico Borba]

Does https://leanprover-community.github.io/100.html update automatically? Or will it just be built whenever the next commit to the website happens?

[Ruben Van de Velde]

I think it's updated daily(?) with the documentation

[Enrico Borba]

Ah, that makes sense. I figured I was just being impatient :)

[Eric Wieser]

Enrico Borba said:

David Loeffler said:

I think Eric meant that your code is unusually well-structured, not that it is structured in an unusual manner :smile:

Hope so! :)

Sorry for the unclear wording, I meant this as praise not criticism!