Zulip Chat Archive

Stream: maths

Topic: physics attack


view this post on Zulip Patrick Massot (Sep 19 2018 at 12:59):

Argg, mathlib is under attack from the physics department!

view this post on Zulip Patrick Massot (Sep 19 2018 at 12:59):

I wasn't expecting that

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:01):

I know Mario doesn't want to have folders cs and math as the first level of the mathlib file hierarchy, but maybe we could have a physics folder

view this post on Zulip Johan Commelin (Sep 19 2018 at 13:03):

Is this referring to the tensor PR :lol: ?

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:03):

Sure

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:03):

it's physics_tensor, there is a typo

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:05):

It's very interesting however that someone outside CS seemed to have been able to learn Lean without coming here on Zulip

view this post on Zulip Johan Commelin (Sep 19 2018 at 13:10):

And it is using tidy! Is this a student of Scott, maybe?

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:11):

The plot thickens

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 13:16):

@Simon Hudon How much of the tensor PR can be done using pi_instances?

view this post on Zulip Johannes Hölzl (Sep 19 2018 at 13:20):

Alex Bentkamp (benti @ github) is a CS PhD student here at the VU. So this is not related to physics. And he got help from me and Rob (his office mate)

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:20):

What about acting stupid and answering we already have tensor products of modules by Kenny?

view this post on Zulip Johannes Hölzl (Sep 19 2018 at 13:21):

why do we need matrices if we have modules?

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:21):

Wow

view this post on Zulip Johannes Hölzl (Sep 19 2018 at 13:25):

its based on the Deep_Learning entry in the AFP: https://www.isa-afp.org/browser_info/current/AFP/Deep_Learning/Tensor.html

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:26):

So today I learned CS people use the word tensor in the same way physicists do

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:27):

Too bad, I was impressed by the story of a physicist learning Lean alone

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:27):

Still, we have matrices but we don't call them linear maps, we call them matrices

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:28):

So we need a different name for tensors and this physics/IA stuff

view this post on Zulip Johannes Hölzl (Sep 19 2018 at 13:32):

IA? is this french for artificial intelligence?

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:32):

sorry, I probably meant AI

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:33):

Yes, wikipedia says AI

view this post on Zulip Johan Commelin (Sep 19 2018 at 13:33):

IA = irtificial antelligence

view this post on Zulip Johannes Hölzl (Sep 19 2018 at 13:33):

@Patrick Massot can you mention the renaming concern on the PR? Alex is usually not here on Zulip

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:33):

yes, it's computer imitating ants who are stupid but exhibit collective intelligence

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:39):

done


Last updated: May 09 2021 at 09:11 UTC