Zulip Chat Archive
Stream: maths
Topic: physics attack
Patrick Massot (Sep 19 2018 at 12:59):
Argg, mathlib is under attack from the physics department!
Patrick Massot (Sep 19 2018 at 12:59):
I wasn't expecting that
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
Johan Commelin (Sep 19 2018 at 13:03):
Is this referring to the tensor PR :lol: ?
Patrick Massot (Sep 19 2018 at 13:03):
Sure
Patrick Massot (Sep 19 2018 at 13:03):
it's physics_tensor, there is a typo
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
Johan Commelin (Sep 19 2018 at 13:10):
And it is using tidy! Is this a student of Scott, maybe?
Patrick Massot (Sep 19 2018 at 13:11):
The plot thickens
Kevin Buzzard (Sep 19 2018 at 13:16):
@Simon Hudon How much of the tensor PR can be done using pi_instances?
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)
Patrick Massot (Sep 19 2018 at 13:20):
What about acting stupid and answering we already have tensor products of modules by Kenny?
Johannes Hölzl (Sep 19 2018 at 13:21):
why do we need matrices if we have modules?
Patrick Massot (Sep 19 2018 at 13:21):
Wow
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
Patrick Massot (Sep 19 2018 at 13:26):
So today I learned CS people use the word tensor in the same way physicists do
Patrick Massot (Sep 19 2018 at 13:27):
Too bad, I was impressed by the story of a physicist learning Lean alone
Patrick Massot (Sep 19 2018 at 13:27):
Still, we have matrices but we don't call them linear maps, we call them matrices
Patrick Massot (Sep 19 2018 at 13:28):
So we need a different name for tensors and this physics/IA stuff
Johannes Hölzl (Sep 19 2018 at 13:32):
IA? is this french for artificial intelligence?
Patrick Massot (Sep 19 2018 at 13:32):
sorry, I probably meant AI
Patrick Massot (Sep 19 2018 at 13:33):
Yes, wikipedia says AI
Johan Commelin (Sep 19 2018 at 13:33):
IA = irtificial antelligence
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
Patrick Massot (Sep 19 2018 at 13:33):
yes, it's computer imitating ants who are stupid but exhibit collective intelligence
Patrick Massot (Sep 19 2018 at 13:39):
done
Last updated: Dec 20 2023 at 11:08 UTC