Melbourne, AU

Stream: Geographic locality

[Yan Yablonovskiy 🇺🇦]

Hey all,

Doubt this will work but trying it out, I saw the Sydney one had a few but did not see a Melbourne.

Might as well post one, maybe there will be someone.

[Geoffrey Irving]

I think some Timaus folk in Melbourne are interested in Lean formalization of singular learning theory, though “interested” means “would be exited if someone did it” rather than “are working on it”.

[neil]

I'm a PhD student at unimelb (though I'm american) and I've just started working with Lean as an alternative to Rocq. There are some others in my department interested in using Lean as well

[Mukesh Tiwari]

Hi @neil , if you don’t mind asking, who at Melbourne is using Lean? (I was a postdoc there with Toby Murray and tried to introduced Rocq during Covid but it didn’t work out. I am just curious how did Lean work out)

[neil]

Vincent Jackson said that he might be working with Lean in the near future, there's another PhD student who's interested in switching from Rocq to Lean, and my supervisors (Christine Rizkallah and Cezary Kaliszyk) are both interested in Lean but I don't think they're planning on working with it

[neil]

I'm the only one I know of actively using Lean as my primary language, but I'm also not that plugged into the department

[neil]

tried to introduce Rocq

You tried to /introduce/ Rocq? I got the sense that Rocq was pretty widely used by people in the department, though I think a lot of stuff I think is written in Rocq is probably actually in Isabelle

[Yan Yablonovskiy 🇺🇦]

If it helps at Monash they do use AGDA in the math department, and i know of some students in CS using Lean here.

[Mukesh Tiwari]

neil said:

tried to introduce Rocq

You tried to /introduce/ Rocq? I got the sense that Rocq was pretty widely used by people in the department, though I think a lot of stuff I think is written in Rocq is probably actually in Isabelle

Thanks! When I was there, it was only Toby who used Isabelle/HOL in computer science department. May be things have changed now.

[neil]

oh, actually, a lot of the people I'm thinking of have come to unimelb in just the past few years... now I feel old

[Mukesh Tiwari]

Christine Rizkallah joined Melbourne just before I moved to Cambridge (I think she joined some time in July/August 2021).

[Moritz Doll]

Somehow I missed this thread.. I am officially working for MQ in Sydney, but I still live in Melbourne and have an office at Unimelb (but the maths department, not compsci).

[Yan Yablonovskiy 🇺🇦]

Moritz Doll said:

Somehow I missed this thread.. I am officially working for MQ in Sydney, but I still live in Melbourne and have an office at Unimelb (but the maths department, not compsci).

I saw you on the lean map, but wasn't sure if it was up to date! So there's at least three of us around :tada:

[Moritz Doll]

Is anyone at AustMS this week?

[Yan Yablonovskiy 🇺🇦]

Unfortunately I cannot make it ! Out of the analysts though, my good friend Yann Bernard will be there and I have been courting him with Lean for a while. In fact his first question was how to encode sobolev spaces.

So maybe if you run into him, he claims to have met you actually and apparently knows Jesse Gell-Redmann well.