九大数理連携チーム

Rational function semifields of dimension one

2025年11月7日(金) 13:30 - 15:30

宋 珠愛 (九州大学 大学院数理学研究院 助教)

Recently some researchers gave many studies toward algebro-geometric foundation for tropical geometry. I focused on rational function semifields of tropical curves and characterized them. With this characterization, in this talk, I suggest a definition of ``rational function semifield of dimension one". This definition can write out weight in the term of $\boldsymbol{T}$-algebra homomorphism, and can write balancing condition together with harmonic functions, where both weight and balancing condition are fundamental concepts for tropical varieties and $\boldsymbol{T}$ is the tropical semifield $(\boldsymbol{R} \cup \{-\infty\}, \operatorname{max}, +)$.

会場: セミナー室 (359号室) / via Zoom

イベント公式言語: 日本語

Introduction to Lean theorem prover

2025年10月31日(金) 14:00 - 17:00

水野 勇磨 (Postdoctoral Researcher, University College Cork, Ireland)

A theorem prover is a tool for the formalization of mathematics, that is, for rigorously expressing and verifying theorems and proofs on a computer. In recent years, the Lean theorem prover has seen progress in the formalization of a wide range of areas of mathematics. In this talk, I will explain formalization of mathematics in Lean from the basics and survey the formalized results achieved to date.

会場: via Zoom / セミナー室 (359号室) 3階 359号室

イベント公式言語: 英語

Computer Algebra with Deep Learning

2025年9月5日(金) 15:00 - 17:00

石原 侑樹 (日本大学 理工学部 数学科 助教)

Computer algebra is a field that aims to perform various mathematical calculations on computers. In recent years, there has been a surge in efforts to accelerate computer algebra algorithms using deep learning models such as “Transformer,” which is used in ChatGPT. In this lecture, I will introduce the results of joint research with Professor Kera et al. on learning Gröbner bases with Transformer.

会場: via Zoom / セミナー室 (359号室) 3階 359号室

イベント公式言語: 英語

Crossroads of Virology and Mathematical Sciences

2025年8月8日(金) 9:30 - 17:30

竹田 誠 (東京大学 大学院医学系研究科 教授)
山次 康幸 (東京大学 農学生命科学研究科 教授)
氣駕 恒太郎 (国立健康危機管理研究機構 室長)
藤田 大士 (京都大学 高等研究院 (KUIAS) 准教授)
小磯 深幸 (九州大学 名誉教授)
黒田 大祐 (日本大学 文理学部 生命科学科 准教授)
カトゥリン・ボシゥメン (理化学研究所 数理創造研究センター (iTHEMS) 副センター長)
谷川 眞一 (東京大学 大学院情報理工学系研究科 准教授)
橋口 隆生 (京都大学 医生物学研究所 教授)
福原 秀雄 (北海道大学 人獣共通感染症国際共同研究所 准教授)
小嶋 将平 (理化学研究所 生命医科学研究センター (IMS) ゲノム免疫生物学理研白眉研究チーム 基礎科学特別研究員)
宮下 脩平 (東北大学 大学院農学研究科 助教)
富安 亮子 (九州大学 マス・フォア・インダストリ研究所 教授)
鈴木 雄太 (国立研究開発法人科学技術振興機構 (JST) 専任研究者)
Adnan Sljoka (理化学研究所 革新知能統合研究センター (AIP))

午前セッション①（ウイルス） 10:00–10:20 麻疹ウイルス工学 竹田 誠（東大 医学系研究科） 10:20–10:40 ポテックスウイルスに対する植物免疫機構 山次 康幸（東大 農学生命科学研究科） 10:40–11:00 ファージの巧妙な感染戦略と細菌の防御応答 氣駕 恒太郎（感染研） 休憩（11:00–11:15） 午前セッション②（分子・数理） 11:15–11:35 多面体型の分子自己集合体を自在に設計する 藤田大士（京大 高等研究院） 11:35–11:55 Anisotropic energy and (curved) polyhedron 小磯 深幸（九大） 11:55–12:15 自然界に倣う二成分タンパク質集合体のデザイン：細胞骨格様構造からウイルス様構造へ 鈴木 雄太（JSTさきがけ） 昼休憩（12:15–13:20） 午後セッション①（計算・数理） 13:20–13:40 Computer-aided antibody design 黒田 大祐（日本大学 生命科学科） 13:40–14:00 Revealing Protein Allostery and Functional Dynamics via Rigidity Theory and NMR Adnan Sljoka（理研 革新知能統合研究センター） 14:00–14:20 Using mathematical models to identify experimental pitfalls when probing virus replication in vitro Catherine Beauchemin（理研 iTHEMS） 14:20–14:40 Combinatorics behind statics and flexibility of graphs 谷川 眞一（東大 情報理工） 休憩（14:40–14:55） 午後セッション②（構造） 14:55–15:15 Glycoprotein structures in human pathogenic RNA viruses 橋口 隆生（京大 医生物） 15:15–15:35 北海道大学におけるクライオ電子顕微鏡設備の紹介 福原 秀雄（北大 人獣共通感染症研） 休憩（15:35–15:50） 午後セッション③（ウイルス・数理） 15:50–16:10 ウイルス感染時の宿主応答のヒト集団遺伝学 小嶋 将平（慶應大 Bio2Q） 16:10–16:30 陸上植物の自殺型抗ウイルス集団抵抗性 宮下 脩平（東北大 農学研究科） 16:30–16:50 Mathematical and crystallographic perspectives in virology 富安 亮子（九大 IMI） 組織委員: Catherine Beauchemin（理研 iTHEMS） 竹田 誠（東大 医学系研究科） 富安 亮子（九大 IMI）

会場: 研究本館 3階 359号室 (メイン会場) / via Zoom

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

2025年8月1日(金) 16:00 - 18:00

恩田 直登 (Project Research Engineer, Research Administrative Division, Omron Sinic X Corporation)

We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach combines rule-based context extraction with LLM-based theorem statement generation, addressing the data scarcity challenge in formal theorem proving. Through iterative generation and evaluation, LeanConjecturer produced 12,289 conjectures from 40 Mathlib seed files, with 3,776 identified as syntactically valid and non-trivial, that is, cannot be proven by aesop tactic. We demonstrate the utility of these generated conjectures for reinforcement learning through Group Relative Policy Optimization (GRPO), showing that targeted training on domain-specific conjectures can enhance theorem proving capabilities. Our approach generates 103.25 novel conjectures per seed file on average, providing a scalable solution for creating training data for theorem proving systems. Our system successfully verified several non-trivial theorems in topology, including properties of semi-open, alpha-open, and pre-open sets, demonstrating its potential for mathematical discovery beyond simple variations of existing results.

会場: via Zoom / セミナー室 (359号室) 3階 359号室

イベント公式言語: 英語

Modeling form growth in curved spaces using Riemannian L-systems

2025年7月17日(木) 16:00 - 17:30

Christophe Godin (Research Derector, Inria, Univ Lyon, France)

In the past 50 years, the formalism of L-systems has been successfully used and developed to model the growth of filamentous and branching biological forms. These simulations take place in classical 2-D or 3-D Euclidean spaces. However, various biological forms actually grow in curved, non-Euclidean, spaces. This is for example the case of vein networks growing within curved leaf blades, of unicellular filaments, such as pollen tubes, growing on curved surfaces to fertilize distant ovules, of teeth patterns growing on folded epithelia of animals, of diffusion of chemical or mechanical signals at the surface of plant or animal tissues, etc. In this talk, I will describe how we extended the formalism of L-systems to model the growth of branching structures in curved spaces. We will discuss how the space may feedback on the growing form and contribute to shape. I will also look at examples, where the space in which the form is growing is not necessarily a surface embedded in the euclidean 3-dimensional space, but is rather a space intrinsically curved, i.e. curved but not embedded in any higher-dimensional space. The possibility to use these more abstract Riemannian spaces potentially opens new avenues for formalizing rules driving the morphogenesis of living forms.

会場: via Zoom / SUURI-COOL (Kyushu)

イベント公式言語: 英語

Quantum Computing Algorithms and Institute of Mathematics-for-Industry

2025年7月3日(木) 15:30 - 17:00

落合 啓之 (九州大学 マス・フォア・インダストリ研究所 教授)

This is the kickoff talk of the Kyushu University Collaboration Team, which aims to foster communication between iTHEMS and IMI. I will introduce some of IMI's activities and organization, as well as my own work, including research on quantum algorithms that began with the launch of the Quantum Computing System Center in 2022.

会場: 研究本館 3階 345-347室

イベント公式言語: 英語