Our debut episode of UnitedReasoning's paper review series is live! 🧠 Dive into the world of theorem proving as we explore how the Proof Strategy Language (PSL) is making proof automation in Isabelle/HOL more accessible.

https://youtu.be/xGQQJKTtgsE

Flood damage has been occurring across Europe, with tragic casualties reported. In Japan, the so-called “Underground Shrine” protects the capital from flooding. I wonder if similar underground facilities will begin to appear in major cities worldwide. As a former Tokyo resident, I’m grateful that such a facility was built and put into operation without becoming a political issue — and all without most of us even noticing.

https://www.bbc.com/future/article/20181129-the-underground-cathedral-protecting-tokyo-from-floods

Renting vs. Owning in the UK: A Personal Reflection

https://unitedreasoning.com/2024/10/20/renting-vs-owning-in-the-uk-a-personal-reflection/

Where is the toilet?

I've recently started using Mapify to add project summaries to my website.

I'm impressed with how this AI tool summarizes my research papers. 😲

Here's an example of a summary for one of my projects on Isabelle/HOL:

https://yutakang.github.io/projects/faster-smarter-induction-for-isabellehol/

I’ve just updated my website! Check out the new clickable graph showcasing dependencies among my current & past projects:

https://yutakang.github.io/research/

The research subpages are still a work in progress. Next, I’ll add insights on the benefits and challenges of each project, reflecting on years of post-completion learning.

“Inspired the README file of the Coqpilot project”
->
“Inspired by the README file of the Coqpilot project”

😢

Inspired the README file of the Coqpilot project, I have added a GIF file to the PSL repository.

While the GIF file is somewhat heavy, it effectively illustrates the functionality of the Abduction Prover clearly. 🤓

For more information:
https://github.com/data61/PSL

I forgot to upload pictures from AITP2024. AITP is still the only CS conference that caused muscle sores to me.

I attended AITP 2024 in Aussois, France 🇫🇷, and gave a talk on the Abduction Prover for Isabelle.

In my talk, I conveyed three key points:
1️⃣ Lemma abduction using modus ponens
2️⃣ Tactics as conjecture
3️⃣ Transition from tree search to graph expansion

You can find the slides here: https://drive.google.com/file/d/1a_668KQODrTsEyAEUiyoORKO_NZTMdDu/view?usp=sharing

At AITP, I learned that a new user group in the USA 🇺🇸 has adopted the TIP benchmark for their deep learning project. Congratulations to Prof. Moa Johansson and the TIP maintenance team in Sweden 🇸🇪 for extending the TIP user groups! 🥳

This event marked the end of my busy summer, during which I traveled from Cambridge 🇬🇧 to Tokyo 🇯🇵, Singapore 🇸🇬, Nancy 🇫🇷, Kutaisi 🇬🇪, Prague 🇨🇿, Bonn 🇩🇪, and Aussois 🇫🇷. 😮‍💨

Now I can finally concentrate on my research. 😎

I recently attended the Trimester Program: Prospect of Formal Mathematics in Bonn, the former capital of West Germany.

For those interested, my presentation "Abduction Prover in Isabelle/HOL" is now available on YouTube: [Yutaka Nagashima: Abduction Prover in Isabelle/HOL](https://www.youtube.com/watch?v=9AlqFnc8QTY).

Additionally, I've made my presentation materials accessible for further reference: [2024_HIM_Yutaka.pdf](https://drive.google.com/file/d/12Rm13_UGlXTOCy2NRpWQd1GS5miCF28x/view?usp=sharing)

It was a rewarding experience to share and discuss advancements in formal mathematics with colleagues in this historic city.

This is my first post on Damus! Excited to join this decentralized platform and connect with others in the tech community. My work focuses on AI for theorem proving, and I have a strong interest in hardware verification. Let's explore the future together! 🚀