日時 ： 2022年2月8日（火） 15:00～16:00
場所 ： 大岡山本館 H213 セミナー室（ハイブリッド開催）
講演者 ： 小松尚夫 氏（浙江理工大学）
題名 ： Linear Diophantine problem of Frobenius associated with number of representations
要旨 ： 与えられた正整数の組(a_1,a_2,...,a_k)に対して、a_1 x_1+a_2 x_2+...+a_k x_k=n という線型方程式の非負整数解(x_1,x_2,...,x_k)を考える。gcd(a_1,a_2,...,a_k)=1であれば、 十分大きい正整数nに対して解は常に存在するから、解が存在しないような最大の整数n (Frobenius数) あるいは解が存在するような最小の非負整数(conductor)に興味がもたれる。 本講演では、Frobenius数 やそれに関連する概念（Sylvester数、Sylvester和、べき和、加重和等）について考察し、既存の結果を基 に新しい結果を与える。また、解がある（１個以上）かない（０個以下）かという元々の問題を拡張して、 解がp個を超えるかp個以下かという問題を考察する。実際、２変数の場合の扱いは容易であり様々な 明示公式が知られているが、３変数以上の場合の扱いは非常に困難になり、特殊な３変数についてわ ずかの結果が知られているに過ぎない。
日時 ： 2021年7月2日, 9日, 16日（金） 15:00～16:00
場所 ： Zoom によるオンライン開催
講演者 ： Johan Commelin 氏（Albert–Ludwigs-Universität Freiburg）
題名 ： Liquid Tensor Experiment
要旨 ： In December 2020, Peter Scholze posed a challenge to formally verify the main theorem on liquid R-vector spaces, which is part of his joint work with Dustin Clausen on condensed mathematics. I took up this challenge with a team of mathematicians to verify the theorem in the Lean proof assistant. Half a year later, we have reached a major milestone, and our expectation is that we are roughly halfway done with the challenge.
The first in this series of three talks will be a colloquium-style talk for a general audience. In this talk I will give a brief motivation for condensed/liquid mathematics, a demonstration of the Lean proof assistant, and discuss our experiences formalizing state-of-the-art research in mathematics.
In the second talk I will give more background on how Lean works. We will see how different components play together to create an extendable interactive proof assistant.
The third talk will give an overview of the proof that we are formalizing. The proof consists of an intricate mix of functional analysis and homological algebra. Instead of getting dragged down in technical inequality estimates, I will try to give a high-level picture of the techniques involved. In particular, I will discuss a simplification of Breen-Deligne resolutions that was discovered during this project.