Zulip Chat Archive

Stream: maths

Topic: (M1M1) Mathematical Methods in Lean


view this post on Zulip Kevin Buzzard (Oct 13 2018 at 11:54):

The joint maths and computer science students at Imperial College London are doing four courses this term. One on Haskell, one on logic, my course M1F, and a course called M1M1, which is a mathematical methods course, where the derivative of sin is cos just like it was at school and nobody really bothers with why that's true.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 11:56):

On the other hand, one of the questions on the first sheet was "define f(x)=1+x+x2/2!+x3/3!+f(x) = 1+x+x^2/2!+x^3/3!+\cdots and let's not worry about what it means to converge. By multiplying everything out and re-arranging without worrying about whether this is valid, prove f(x+y)=f(x)×f(y)f(x+y) = f(x) \times f(y)"

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 11:57):

and I thought " @Chris Hughes did that properly, took him ages"

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 11:57):

I wonder how far we'll be able to get on the M1M1 example sheets by the end of term :-)

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 11:58):

One of the questions needed log and Chris did that a few weeks ago, so we're still just ahead

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 11:59):

Are double angle formulae in Lean? Tricks about sin(theta) in terms of tan(theta/2)?

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:00):

Stuff which is assumed in M1M1? Ability to define 0ex2/2dx\int_0^\infty e^{-x^2/2} d x?

view this post on Zulip Chris Hughes (Oct 13 2018 at 12:04):

It's not just methods that's like this. Try formally proving every permutation is the product of disjoint cycles.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:09):

you show us up for the charlatains we are!

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:10):

But we're mathematicans. If your silly software cannot easily prove things which are intuitively obvious to us then the problem is surely with your software

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:11):

The proof is "choose an element, keep hitting with the permutation, eventually you'll get back to where you start, done by induction"

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:12):

(assuming we're talking about finite sets/types)

view this post on Zulip Kenny Lau (Oct 13 2018 at 12:16):

that's what I did

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:19):

how many lines?

view this post on Zulip Kenny Lau (Oct 13 2018 at 12:32):

26 lines

view this post on Zulip Kenny Lau (Oct 13 2018 at 12:32):

https://github.com/kckennylau/Lean/blob/master/Sym.lean#L645-L670

view this post on Zulip Kenny Lau (Oct 13 2018 at 12:32):

def list_step (σ : Sym n) : list (step n) :=
by refine well_founded.fix list_step.aux.wf _ σ; from
λ σ ih, if H : σ.support =  then []
  else let i, hi := σ.support_choice H in
    step.mk' (σ i) i (support_def.1 hi)
    :: ih (swap (σ i) i * σ) (support_swap_mul hi)

@[simp] lemma list_step_prod (σ : Sym n) :
  (σ.list_step.map step.eval).prod = σ :=
well_founded.induction list_step.aux.wf σ $ λ σ ih,
begin
  dsimp [list_step],
  rw [well_founded.fix_eq],
  split_ifs,
  { ext, by_contra H,
    suffices : i  ( : finset (fin n)),
    { simp at this, cc },
    rw [ h, support_def],
    exact mt eq.symm H },
  cases support_choice σ h with i hi,
  unfold list_step._match_1,
  specialize ih _ (support_swap_mul hi),
  dsimp [list_step] at ih,
  rw [list.map_cons, list.prod_cons, ih,  mul_assoc],
  rw [step.eval_mk', swap_mul_self, one_mul]
end

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:32):

That sounds like a reasonable length to me.

view this post on Zulip Chris Hughes (Oct 13 2018 at 12:38):

That's a proof of something different isn't it? It's a proof about products of swaps, not disjoint cycles.

view this post on Zulip Kenny Lau (Oct 13 2018 at 12:43):

ah, right

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 12:45):

so the question remains

view this post on Zulip Chris Hughes (Oct 13 2018 at 21:17):

225 lines https://github.com/leanprover/mathlib/compare/master...dorhinj:cycles2?expand=1

view this post on Zulip Mario Carneiro (Oct 13 2018 at 23:45):

I like it, we're getting a lot of nice structure on perm

view this post on Zulip Mario Carneiro (Oct 13 2018 at 23:46):

Any chance of defining stuff about the finitely supported permutations? (i.e. it's a subgroup, and has most of the properties you have put on finite permutation groups like the alternating group or separation into disjoint cycles)

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 10:09):

One would imagine that these are also situations where a mathematician would say "it's obvious" (like e.g. the fact that it's a subgroup).

view this post on Zulip Kenny Lau (Oct 14 2018 at 10:10):

I think at this point we all know that it's pointless to keep saying that so and so is obvious to a mathematician.

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 10:13):

I don't think it's pointless at all Kenny. I think that if we isolate many of the things that are "obvious to a mathematician" and make sure that they are relatively easy for a mathematician do in Lean (even though we all know that they are in truth difficult to do from the actual axioms of mathematics) then this is a step towards making Lean more intuitive for mathematicians to use.

view this post on Zulip Chris Hughes (Oct 14 2018 at 12:26):

Any chance of defining stuff about the finitely supported permutations? (i.e. it's a subgroup, and has most of the properties you have put on finite permutation groups like the alternating group or separation into disjoint cycles)

What's the best approach for this. Are you happy to lose computability in favour of generality? My cycle_of function can certainly be extended to infinite permutations, but not computably, though it is outrageously slow anyway. For sign and stuff, is it best to just create a new definition of sign for finitely supported permutations of infinite types. I imagine this is better than making a partial function which is actually a total function on most of the stuff people want to use it for.

view this post on Zulip Mario Carneiro (Oct 14 2018 at 12:31):

cycle_of should be computable on infinite (finitely supported) permutations, assuming decidable_eq on the base set, although I would factor it into a cycle_support function that returns the list of iterates of the input

view this post on Zulip Mario Carneiro (Oct 14 2018 at 12:34):

and then I guess there are also a bunch of noncomputable functions we might want in the truly infinite case, like cycle_of where the cycle is possibly isomorphic to Z

view this post on Zulip Mario Carneiro (Oct 14 2018 at 12:36):

In fact it is still true that "every permutation is a product of cycles" in the truly infinite case, you just have to make sense of an infinite product of disjoint permutations

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 13:22):

I think at this point we all know that it's pointless to keep saying that so and so is obvious to a mathematician.

Just adding to this thread that to a 1st year maths undergraduate it is "obvious" that the derivative of sin(x)\sin(x) is cos(x)\cos(x) (because they "learnt it at school") and I think that having this in Lean would be a very natural goal. It will be interesting to see if our new cohort of freshers were up to the task.


Last updated: May 10 2021 at 08:14 UTC