## Stream: general

### Topic: random math question

#### Andrew Ashworth (Mar 31 2018 at 18:51):

so, seeing as how there are many mathematicians here, can anyone recommend a textbook on algebraic topology? I'd like to be able to read https://arxiv.org/pdf/1802.04443.pdf

#### Kenny Lau (Mar 31 2018 at 18:51):

Hatcher, of course

#### Kenny Lau (Mar 31 2018 at 18:54):

@Andrew Ashworth Hatcher Chapter 2

#### Andrew Ashworth (Mar 31 2018 at 18:56):

thanks, i'll check it out

#### Simon Hudon (Mar 31 2018 at 18:58):

@Andrew Ashworth Are you taking on Machine Learning as a hobby? I've been contemplating getting literate in the domain. There seems to be a lot to be done there. I'm curious about proving security / safety properties in those systems but I still don't know where to start

#### Andrew Ashworth (Mar 31 2018 at 19:02):

i work in imaging and radar

#### Andrew Ashworth (Mar 31 2018 at 19:03):

are you looking for textbook recommendations? that's where i started off

#### Simon Hudon (Mar 31 2018 at 19:03):

Interesting. ML must be useful but tricky thing to use there

Yes, thanks!

#### Kenny Lau (Mar 31 2018 at 19:04):

how would you name the groups that can be generated by a set that injects to S?

#### Kenny Lau (Mar 31 2018 at 19:04):

as in, name them in Lean

What is S?

a random set

#### Andrew Ashworth (Mar 31 2018 at 19:06):

i'd start off with the elements of statistical learning

#### Kenny Lau (Mar 31 2018 at 19:06):

@Simon Hudon I just need a short name

you know

#### Simon Hudon (Mar 31 2018 at 19:07):

So when you say "injects" I assume you have an injective function from S to S?

#### Simon Hudon (Mar 31 2018 at 19:07):

Actually, if you show me the construction, that would help me find a name for it

#### Kenny Lau (Mar 31 2018 at 19:07):

I mean, a group G is inside my structure if it is generated by a set T with an injection from T to S

#### Simon Hudon (Mar 31 2018 at 19:09):

Ok, that's clearer. Is that group interesting because of your choice of S and then the group basically says that the set T exists and is the set underlying G?

#### Kenny Lau (Mar 31 2018 at 19:10):

structure to_be_named (G : Type u) [group G] :=
( gen : set G )
( gen_gen : group.generate gen = set.univ )
( func : gen → S )
( inj : function.injective func )


#### Simon Hudon (Mar 31 2018 at 19:10):

i'd start off with the elements of statistical learning

Thanks! Do you plan on doing some ML in Lean?

#### Kenny Lau (Mar 31 2018 at 19:16):

@Simon Hudon do you have any suggestions?

#### Andrew Ashworth (Mar 31 2018 at 19:16):

that would be really hard without a good way of handling algebra and probability

#### Andrew Ashworth (Mar 31 2018 at 19:16):

er, by algebra i mean matrices

Last updated: Dec 20 2023 at 11:08 UTC