A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL (FM 2026 - Workshop: AIPV) - FM 2026

Mon 18 - Fri 22 May 2026 Tokyo, Japan

Who

Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li, Conrad Watt

Track

FM 2026 Workshop: AIPV

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Mon 18 May 2026 12:00 - 12:20 at 1F Room 101-103 - AIPV Day 1 Session 2 Isabelle & Rocq

Qiyuan Xu

Nanyang Technological University

Renxi Wang

MBZUAI

United Arab Emirates

Peixin Wang

East China Normal University

Haonan Li

MBZUAI

Conrad Watt

Nanyang Technological University

Singapore

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Mon 18 May
Displayed time zone: Osaka, Sapporo, Tokyo change

	11:00 - 12:40	AIPV Day 1 Session 2 Isabelle & RocqWorkshop: AIPV at 1F Room 101-103

	11:00 20m Talk		Automated Sketching and Repairing of Large Mechanised Proofs Workshop: AIPV Chengsong Tan Kaihong, Jonathan Julian Huerta y Munive Aalborg University in Copenhagen, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London
	11:20 20m Talk		Inverting the Formalization Workflow: Prototyping an MPC Protocol in Rocq with an LLM Agent Workshop: AIPV Cheng-Hui Weng Nagoya University
	11:40 20m Talk		Formalizing Actuarial Mathematics in Proof Assistants Workshop: AIPV Yosuke Ito Sompo Himawari Life Insurance Inc.
	12:00 20m Talk		A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL Workshop: AIPV Qiyuan Xu Nanyang Technological University, Renxi Wang MBZUAI, Peixin Wang East China Normal University, Haonan Li MBZUAI, Conrad Watt Nanyang Technological University
	12:20 20m Talk		Sponsor Talk by Harmonic: Automatically Formally Verified Software using Aristotle Workshop: AIPV