Tokyo, JP

Stream: Geographic locality

[Yuma Mizuno]

:wave:

[furea2]

Hello, I'm working in Tokyo and glad to see anyone in Zulip. My major was stable homotopy theory.

[Samuel Levi Schmidt]

Hello :smile:

I am going to be at the National Institute of Informatics for the next months. Hmu if you are interested in Lean and are in the area.

[Miyahara Kō]

Hello :hello:
I joined this community in 2023/02/02. Sorry for the late greeting.

[Asei Inoue]

こんにちは :smile:
私は東京で働いています．Lean に関する日本語の情報を集積する活動をしていて，
こういうものを作っています．よろしくお願いします．

Hello :smile:
I'm working in Tokyo. I'm working on making a collection of information on Lean in Japanese, and I've created this.

https://lean-ja.github.io/tactic-cheatsheet/

[Mario Carneiro]

全般的には、 https://github.com/lean-ja のは日本語のリーン ユーザーにとって役立つ情報がたくさんあります。もっと広く広めるべきと思います。

More generally, https://github.com/lean-ja has a bunch of useful information for lean users in japanese, I think we should re-share it more widely.

[Mario Carneiro]

Maybe there should be a link on the website https://leanprover-community.github.io/ to language-specific communities?

[Florent Schaffhauser]

Asei Inoue said:

https://lean-ja.github.io/tactic-cheatsheet/

すごいですね！今度東京に行ったら、会えるかも知れないね :blush:

[Asei Inoue]

旧タクティク逆引きリストではタクティクをメインに紹介していましたが、それ以外にもコマンドや型クラスなども紹介するようになりました。
それに合わせて名前も Lean by Example と変更しました。
日本における Lean の普及に資するべく内容を充実させていこうと思っています。

The old "tactic cheatsheet" mainly presented tactics, but now also commands and typeclasses, and so on.
The name was changed accordingly to "Lean by Example".
We intend to enhance the content with the aim of spreading Lean in Japan.

https://lean-ja.github.io/lean-by-example/

[Agnishom Chattopadhyay]

I recently moved to Tokyo as well! I work at Imiron (https://imiron.io/)

[Asei Inoue]

いいですね。よろしければ Imiron という会社のことをもっと教えてください。
nice! If you don't mind, please tell us more about the company Imiron. :hug:

[Agnishom Chattopadhyay]

We implement tools and algorithms based on formal method techniques. Most of the current team at Imiron previously worked at the ERATO-MMSD group with Prof. Hasuo

[Agnishom Chattopadhyay]

We are hosting a Haskell meetup in February, if anyone is interested: https://www.meetup.com/tokyo-haskell-meetup/events/305838131/

[Asei Inoue]

Haskell meetup 楽しかったです。教えてくれてありがとうございました。
I have enjoyed Haskell meetup! Thanks!

[Asei Inoue]

https://lean-ja.github.io/lean-by-example/

Lean by Example はまだまだ更新中です。扱う範囲はどんどん広がってきていて、今は私が Lean について知っていることのすべてをここに記載したいなと考えています。皆さんの調べ物に使っていただければ嬉しいです。

Lean by Example is still being updated. The scope is gradually expanding, and I hope to include everything I know about Lean here. I would be happy if you find it useful for your learning.

[Asei Inoue]

https://www.lambdanote.com/products/n-vol-5-no-1

n 月刊ラムダノートに、Lean の記事を寄稿しました！

I contributed an article on Lean to n monthly Lambda Note! This is one of the few articles about Lean published in Japanese.

[Kevin Buzzard]

Is the article freely available?

[Asei Inoue]

@Kevin Buzzard

Is the article freely available?

paid only, sorry
do you want to read it?

[Kevin Buzzard]

I was just curious, because it seems to be about implementing natural numbers, and I'm always keen to hear other people's opinions on this.

[Asei Inoue]

@Kevin Buzzard

Indeed, I was very influenced by your Natural Number Game to write that article.

Can't I buy it from outside of Japan? you can download it as a PDF, so you should be able to use machine translation.