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.

iTHEMS Cosmology Forum Workshop is a series of short workshops, each focusing on an emerging topics in cosmology. The target audience is cosmologists, high-energy physicists and astronomers interested in learning about the subject, not just those who have already worked on the topic. The goal of the workshop is to provide working knowledge of the topic and leave dedicated time for discussions to encourage mutual interactions among participants.

The fourth workshop is dedicated to new physics discoveries enabled by new spectroscopic data. Nearly three decades after the discovery of accelerated expansion, there is at last compelling data pointing away from the simple cosmological constant. The results of new data hint at evolving dark energy, but the statistical significance and physical interpretation are both far from clear. Furthermore, another anticipated new physics measurement of the neutrino mass has also proven difficult. With this workshop, we aim to interrogate both the statistical evidence for new physics as well as the theoretical implications if these new results are confirmed.

This forum will consist of two days.

The workshop will be in English.

The workshops are organised by the iTHEMS Cosmology Forum working group, which is the successor of the Dark Matter Working Group at RIKEN iTHEMS.

Important dates:
July 18 - Registration deadline
August 4th, 5th - Workshop Days

Invited Speakers:
Sesh Nadathur (University of Portsmouth)
Andrei Cuceu (LBNL)
Gerrit Farren (LBNL)
Antonio De Felice (YITP)
Linda Blot (IPMU)
Wen Yin (TMU)

The seminar will be jointly given by Associate Professor Dai Yamazaki (The university of Tokyo) and Professor Hannah Cloke (University of Reading).

Speaker 1: Associate Professor Dai Yamazaki (Institute of Industrial Science, The University of Tokyo)
Title: How can we achieve fast and realistic simulation of river and flood dynamics on the global scale?
Abstract: Modeling river hydrodynamics across continental-scale basins is challenging due to their inherently multiscale nature. On one hand, we must account for the water budget along river systems that extend over 1,000 km. On the other hand, water movement within channels and floodplains is governed by topographic features smaller than 100 meters. The global river model CaMa-Flood addresses this complexity by employing the Catchment-based Macro-scale Floodplain modeling approach (CMF approach). This method approximates the relationship between water volume, flood extent, and water depth through sub-grid scale parameterizations. These parameters, derived from high-resolution satellite-based digital elevation models (DEMs) and hydrography datasets, enable realistic simulation of river discharge and flood stages—without explicitly resolving small-scale floodplain dynamics. To further accelerate simulations, recent developments in CaMa-Flood have introduced several performance optimizations, including MPI/OpenMP parallelization, SIMD vectorization, sparse matrix implementation, and a GPU-enabled Python version. These enhancements make the model more suitable for large-scale and near-real-time applications such as global flood monitoring and climate impact assessment.

Speaker 2: Professor Hannah Cloke (Department of Meteorology, University of Reading)
Title: Preparing for floods in an uncertain future

This meeting will be used to welcome another new members to the iTHEMS Biology Study Group: Dr. Sungsik Kong, who is joining iTHEMS Fundamental Division as a Research Scientist. He will give us a 15-20 min talk to introduce his research. If time permits, let's also use this time to catch up on each other's current research. I hope that many people will join us to welcome this new member and come meet him and hear about his research.

By creating a shared space for dialogue, we aim to stimulate new research directions and foster collaborative insights through the integration of mathematical sciences into studies of both the structural principles that govern viral form and function, and the dynamics of viral replication. We invite participation from both mathematical and theoretical scientists interested in the structure and replication mechanisms of viruses, as well as virologists who are open to exploring the potential of mathematical abstraction.

Program:

Morning Session I (Viruses)
10:00–10:20 Measles virus engineering
Makoto Takeda (The University of Tokyo, Graduate School of Medicine)
10:20–10:40 Plant immunity to potexviruses
Yasuyuki Yamaji (The University of Tokyo, Graduate School of Agricultural and Life Sciences)
10:40–11:00 Sophisticated phage infection strategies and bacterial defense responses
Kotaro Kiga (National Institute of Infectious Diseases)
Break (11:00–11:15)
Morning Session II (Molecules, Math)
11:15–11:35 Designing Polyhedral Molecular Architectures at Will
Daishi Fujita (Kyoto University, Institute for Advanced Study)
11:35–11:55 Anisotropic energy and (curved) polyhedron
Miyuki Koiso (Kyushu University)
11:55–12:15 Nature-Inspired Design of Two-Component Protein Assemblies: From Cytoskeleton-Like to Virus-Like Structures
Yuta Suzuki (JST PRESTO)
Lunch Break (12:15–13:20)

Afternoon Session I (Comp Sci, Math)
13:20–13:40 Computer-aided antibody design
Daisuke Kuroda (Nihon University, Department of Life Sciences)
13:40–14:00 Revealing Protein Allostery and Functional Dynamics via Rigidity Theory and NMR
Adnan Sljoka（RIKEN AIP）
14:00–14:20 Using mathematical models to identify experimental pitfalls when probing virus replication in vitro
Catherine Beauchemin (RIKEN iTHEMS)
14:20–14:40 Combinatorics behind statics and flexibility of graphs
Shinichi Tanigawa (The University of Tokyo, Graduate School of Information Science and Technology)
Break (14:40–14:55)
Afternoon Session II (Structures)
14:55–15:15 Glycoprotein structures in human pathogenic RNA viruses
Takao Hashiguchi (Kyoto University, Graduate School of Medicine and Biomedical Sciences)
15:15–15:35 Introduction of cryo-electron microscopy facilities at Hokkaido University
Hideo Fukuhara (Hokkaido University, Research Center for Zoonosis Control)
Break (15:35–15:50)
Afternoon Session III (Viruses, Math)
15:50–16:10 Human genetics during virus infection
Shohei Kojima (Keio University, Bio2Q)
16:10–16:30 Suicidal population resistance of land plants against viruses
Shuhei Miyashita (Tohoku University, Graduate School of Agricultural Science)
16:30–16:50 Mathematical and crystallographic perspectives in virology
Ryoko Tomiyasu (Kyushu University, IMI)

Organizers:
Catherine Beauchemin (RIKEN iTHEMS)
Makoto Takeda (University of Tokyo, Graduate School of Medicine)
Ryoko Tomiyasu (Kyushu University, IMI)

This workshop aims to strengthen collaboration between researchers at RIKEN iTHEMS and the National Center for Theoretical Sciences in Taiwan. It will be a four-day event, with the first two days dedicated to interdisciplinary topics. The last two days will focus on specialized areas, with one day devoted to condensed matter physics and the other to high-energy physics, including quantum gravity.

The geometric Langlands correspondence (GLC) is a geometric analogue of the Langlands conjecture in number theory, relating algebraic geometry, representation theory, and many other areas. Since A. Kapustin and E. Witten pointed out the relation between GLC and mirror symmetry, there have been various studies on GLC from a physics perspective as well as a mathematical perspective.

First talk: An introduction to Langlands conjecture for everyone
This is an entirely accessible overview of the Langlands conjecture. Starting from famous topics, such as the Pythagorean theorem and Fermat’s Last Theorem, I will introduce the statement and motivations behind the Langlands conjecture.
No prior background will be assumed, and technical details will often be sketched rather than fully developed, so that anyone with a general mathematical curiosity can follow along.

Second talk: On a certain tamely ramified geometric Langlands correspondence
In this talk, I will present my research. Arinkin’s 2001 result established the geometric Langlands correspondence for the case G = SL2 on the complex projective line P1 with four fixed regular singularities. When one attempts to extend this to five or more singularities, it turns out to be more natural to decompose the correspondence into a Radon transform-type correspondence and a “GLC‑like” correspondence.
I will report on the calculations of cohomology that support the proof of this GLC‑like correspondence in the P1 with five fixed regular singularities case.

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.

[Scientific scope]
The symposium will address experimental and theoretical investigations of the equation-of-state (EoS) of nuclear matter at various isospin asymmetries. Such investigations include efforts in nuclear structure, nuclear reactions and heavy-ion collisions, as well as in astrophysical observations of compact stars and associated phenomena. An important role of the symposium is to unify efforts of the nuclear physics and astrophysics communities in addressing common research challenges.

Quantum reference frames (QRFs) are a universal tool for dealing with symmetries in quantum systems. Roughly speaking, they are internal subsystems that transform in some non-trivial way under the symmetry group of interest and constitute the means for describing quantum systems from the inside in purely relational terms. QRFs are thus crucial for describing and extracting physics whenever no external reference frame for the symmetry group is available. This is in particular the case when the symmetries are gauge, as in gauge theory and gravity, where QRFs arise whenever building physical observables. The choice of internal QRF is typically non-unique, giving rise to a novel quantum form of covariance of physical properties under QRF transformations. This lecture series will explore this novel perspective in detail with a specific emphasis on applications in high-energy physics and gravity.

I will begin by introducing QRFs in mechanical setups and explain how they give rise to quantum structures of covariance that mimic those underlying special relativity. I will explain how this leads to subsystem relativity, the insight that different QRF decompose the total system in different ways into gauge-invariant subsystems, and how this leads to the QRF dependence of correlations, entropies, and thermal properties. We will then explore how relational dynamics in Hamiltonian constrained systems and the infamous "problem of time" can be addressed with clocks identified as temporal QRFs. In transitioning to the field theory setting, we will first consider hybrid scenarios, where QRFs are quantum mechanical, but the remaining degrees of freedom are quantum fields including gravitons. I will explain how this encompasses the recent discussion of "observers", generalized entropies, and gravitational von Neumann algebras by Witten et al. and how subsystem relativity leads to the conclusion that gravitational entanglement entropies are observer dependent. We will then discuss the classical analog of QRFs in gauge theory and gravity and how they can be used to build gauge-invariant relational observables and to describe local subsystems. This will connect with discussions on edge and soft modes in the literature, the former of which turn out to be QRFs as well. This has bearing on entanglement entropies in gauge theories, which I will describe on the lattice, providing a novel relational construction that overcomes the challenges faced by previous constructions, which yielded non-distillable contributions to the entropy and can be recovered as the intersection of "all QRF perspectives". Finally, I will describe how the classical discussion of dynamical reference frames can be used to build a manifestly gauge-invariant path integral formulation that opens up novel relational perspectives on effective actions and the renormalization group in gravitational contexts, which is typically plagued by a lack of manifest diffeomorphism-invariance. I will conclude with open questions and challenges in the field.

Program:

September 24
10:15 - 10:30 Registration and reception with coffee
10:30 - 12:00 Lecture 1
12:00 - 13:30 Lunch
13:30 - 15:00 Lecture 2
15:00 - 16:00 Coffee break
16:00 - 17:00 Lecture 3
17:10 - 18:10 Short talk session
18:20 - 21.00 Banquet

September 25
10:15 - 10:30 Morning discussion with coffee
10:30 - 12:00 Lecture 4
12:00 - 13:30 Lunch
13:30 - 15:00 Lecture 5
15:00 - 16:00 Coffee break
16:00 - 17:00 Lecture 6
17:10 - 18:10 Short talk session

September 26
10:15 - 10:30 Morning discussion with coffee
10:30 - 12:00 Lecture 7
12:00 - 13:30 Lunch
13:30 - 15:00 Lecture 8
15:00 - 16:00 Coffee break
16:00 - 17:00 Lecture 9 & Closing

(The deadline of the registration is on Sep 30.)

100 years have passed since quantum mechanics was born. The mathematical model has been describing the physical world remarkably well. However, the foundations of this model still remain unclear. A comprehensive understanding of quantum theory, including its foundations, is becoming even more important in an era where the demands of realizing quantum information technologies pose significant theoretical and experimental challenges.

The framework of General Probabilistic Theories (GPTs) is a modern approach to the foundations of quantum theory. It deals with mathematical generalizations of both classical and quantum theories and has attracted increasing attention in recent years. Roughly speaking, research on GPTs has three major objectives: characterizing the models of classical and quantum theories, investigating the fundamental limits of physical and information-theoretic properties arising from operational requirements, and deepening our understanding of the mathematical structures underlying classical and quantum theories. The studies of GPTs have provided many new perspectives on these topics. However, at the same time, there remain many important open problems in the field. For this reason, more researchers are encouraged to enter and contribute to research on GPTs.

This intensive three-day lecture series is designed to provide researchers and graduate students with the essential knowledge necessary for research on GPTs, starting from an introduction to the subject. The lectures will cover the mathematical foundations, physical and information-theoretic concepts, and both the established results and future directions of GPT research. The 1st day will present the necessary mathematical structures, including convex geometry, positive cones, and the operational formulation of probabilistic models. The 2nd day will explore composite systems, information-theoretic quantities, symmetries, and Euclidean Jordan algebras. The 3rd day will survey key results on discrimination and communication tasks, the characterization of classical and quantum theories, and open problems that connect GPTs to quantum information science and beyond.

Note: The content of each lecture may extend into the next slot or be covered earlier, depending on the pace of discussion and participant questions.

The 1st day (6th Oct.): Mathematical Introduction to GPTs
Venue: Large Meeting Room, 2F, Wako Welfare & Conference Building
10:30-12:00 Lecture 1 (Introduction and Mathematics on Positive Cones)
12:00-13:30 Lunch time
13:30-15:00 Lecture 2 (Mathematics on Positive Cones)
15:00-15:30 Coffee break
15:30-17:00 Lecture 3 (Introduction to General Models and Relation between Operational Probability Theories)

The 2nd day (7th Oct.): Physical and Information Theoretical Concepts in GPTs
Venue: Large Meeting Room, 2F, Wako Welfare & Conference Building
10:30-12:00 Lecture 4 (Composite Systems in GPTs)
12:00-13:30 Lunch time
13:30-15:00 Lecture 5 (Information Quantities)
15:00-15:30 Coffee break
15:30-17:00 Lecture 6 (Dynamics, Symmetry, and Euclidean Jordan Algebras)

The 3rd day (8th Oct): Previous and Future Studies in GPTs
Venue: Meeting Room 435-437, 4F, Wako Main Research Building
10:30-12:00 Lecture 7 (Discrimination and Communication Tasks)
12:00-13:30 Lunch time
13:30-15:00 Lecture 8 (Characterization of Classical and Quantum Theories)
15:00-15:30 Coffee break
15:30-17:00 Lecture 9 (Other Topics, Open Problems, and Future Directions)
18:00- Dinner

The day of no lecture (9th Oct): Open Discussion and Q&A
Research discussions will take place between the lecturer and participants in areas such as the hallways on the 3rd and 4th floors of the Main Research Bldg, RIKEN Wako Campus.