Birthday problem

Stream: maths

[Mario Carneiro]

I see that the birthday problem is listed at https://leanprover-community.github.io/100.html#93 but the theorem statement is a far cry from it:

theorem fintype.card_embedding_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [fintype (α ↪ β)] :
  fintype.card (α ↪ β) = (fintype.card β).desc_factorial (fintype.card α)

I would expect the full problem to include not just this fact but also the total number of functions from A to B, and then some numerical computation to show that fewer than half of the functions from fin 23 to fin 365 are injective.

[Mario Carneiro]

cc: @Eric Rodriguez

[Ruben Van de Velde]

That's in archive/100-theorems-list/93_birthday_problem.lean

[Kevin Buzzard]

Freek is pretty lenient about what counts :-) Last time I looked, one of the "proofs of Pythagoras' theorem" was a definition of the distance on $\R^2$ for example.

[Kevin Buzzard]

But I agree we could do better :-)

[Mario Carneiro]

I know that, but that doesn't mean we should be too

[Mario Carneiro]

indeed the archive version is much better:

theorem birthday :
  2 * ‖fin 23 ↪ fin 365‖ < ‖fin 23 → fin 365‖ ∧ 2 * ‖fin 22 ↪ fin 365‖ > ‖fin 22 → fin 365‖

that should be on the web page

[Mario Carneiro]

Also a bunch of them have links but no statements on the page, what's up with that?

[Alex J. Best]

In a similar vein we have "the Pell equation" but only for d that are one less than a square. It would be a really nice project for someone to solve the full Pell equation sometime

[Yaël Dillies]

Wasn't this done on Xena this summer?

[Eric Rodriguez]

The archive version was actually a bit more work, as I had to develop the theory of the desc_factorial in order to even get Lean to be able to evaluate the numbers

[Eric Rodriguez]

I was hoping to state in terms of probability theory at some point, too, should be relatively easy with the counting measure. I'll update the yaml file when I can sit down at a computer

[Kevin Buzzard]

@Harun Khan was working on Pell. I think he got everything: the fundamental unit and a proof that all solutions were up to sign a power of the fundamental unit. Unfortunately he's graduated from Imperial now and is at Stanford doing machine learning :-) I'll see if I can get in touch with him and find out the status of the project.

[Kevin Buzzard]

He says it's not public yet but he hopes to make it public within the next couple of weeks

[Eric Rodriguez]

Mario Carneiro said:

Also a bunch of them have links but no statements on the page, what's up with that?

I think this is to do with the fact archive is separate, sadly

[Mario Carneiro]

Is this file automatically generated? I wouldn't expect it to be

[Eric Rodriguez]

I've removed the misleading decl and added some more stuff at #16528

[Eric Rodriguez]

Yes, it's generated automatically from 100.yaml

[Eric Rodriguez]

I think maybe a manual override to provide some lean code and a link for the cases where it doesn't work would be nice, though

[Mario Carneiro]

yeah, I'm thinking to add another key containing markdown to inject in the document

[Mario Carneiro]

where's the generator script?

[Eric Rodriguez]

they seem to be yaml_check.py/.lean, but they seem a bit small for doing the job they do