Welcome!
The G-Research Technology Innovation Group scouts emerging technologies that have the potential to transform quantitative finance.
In this blog, we share some of our early explorations into Lean 4 (an interactive theorem prover and programming language) and large language models (LLMs) trained to work with Lean 4. Our goal is to introduce readers to some of the practical insights and background knowledge we’ve gathered—things that aren’t always easy to find, but that help fill in important gaps when entering this field. Over the past few months, we’ve been reading papers, experimenting with datasets, and running our own model tests in collaboration with academic researchers, and these posts capture some of the lessons learned along the way. While our long-term aim is to publish more formal research, this blog offers a snapshot of the ideas and experiments that we’ve been developing to date.
Datasets
Explore various datasets used for training and evaluating Lean 4 models.
Repl Cryogenics
Using CRIU for REPL checkpointing.