Math & Computer Seminar
6 events
-
Seminar
Median-based estimators for randomized quasi-Monte Carlo integration
January 9 (Fri) 15:00 - 17:00, 2026
Kosuke Suzuki (Associate Professor, Yamagata University)
High-dimensional numerical integration is a ubiquitous challenge across various fields, from mathematical finance to computational physics and Bayesian statistics. While standard Monte Carlo (MC) methods are robust, their probabilistic error convergence rate of $O(N^{-1/2})$ is often insufficient for demanding applications. In this talk, I will introduce Quasi-Monte Carlo (QMC) and Randomized QMC (RQMC) methods, which offer a powerful framework for accelerating integration using low-discrepancy point sets. A key advantage of this deterministic approach is its ability to achieve a convergence rate of $O(N^{-1+\epsilon})$, significantly outperforming the standard MC rate. The second part of the talk will focus on the construction of point sets, specifically lattice rules and digital nets. I will explain how these methods achieve higher-order convergence rates, faster than $O(N^{-1})$, for sufficiently smooth integrands. I will also discuss their randomized variants and demonstrate how RQMC with mean-based estimators provides practical error estimation while maintaining high-order convergence. Finally, I will discuss recent progress in RQMC involving median-based estimators. I will highlight how these estimators achieve almost optimal convergence rates for various function spaces without requiring prior knowledge of the integrand.
Venue: Hybrid Format (3F #359 and Zoom), Seminar Room #359
Event Official Language: English
-
Seminar
Rational function semifields of dimension one
November 7 (Fri) 13:30 - 15:30, 2025
JuAe Song (Assistant Professor, Faculty of Mathematics, Kyushu University)
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}, +)$.
Venue: Seminar Room #359 / via Zoom
Event Official Language: Japanese
-
Seminar
Introduction to Lean theorem prover
October 31 (Fri) 14:00 - 17:00, 2025
Yuma Mizuno (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.
Venue: via Zoom / #359, Seminar Room #359
Event Official Language: English
-
Seminar
Computer Algebra with Deep Learning
September 5 (Fri) 15:00 - 17:00, 2025
Yuki Ishihara (Assistant Professor, Department of Mathematics, College and Science Technology, Nihon University)
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.
Venue: via Zoom / #359, Seminar Room #359
Event Official Language: English
-
Seminar
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
August 1 (Fri) 16:00 - 18:00, 2025
Naoto Onda (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.
Venue: via Zoom / #359, Seminar Room #359
Event Official Language: English
-
Seminar
Quantum Computing Algorithms and Institute of Mathematics-for-Industry
July 3 (Thu) 15:30 - 17:00, 2025
Hiroyuki Ochiai (Professor, Institute of Mathematics for Industry, Kyushu University)
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.
Venue: #345-347, 3F, Main Research Building
Event Official Language: English
6 events