Learning Mathematics with Lean By Yuki Otsuka

議題

TR514 [[ new Date( '2024-08-04 02:45:00+00:00' ).toLocaleDateString('ja', {year: 'numeric', month: '2-digit', day: '2-digit'}) ]] [[ new Date( '2024-08-04 02:45:00+00:00' ).toLocaleTimeString('zh-Hant', {hour12: false, hour: '2-digit', minute:'2-digit'}) ]] ~ [[ new Date( '2024-08-04 03:15:00+00:00' ).toLocaleTimeString('zh-Hant', {hour12: false, hour: '2-digit', minute:'2-digit'}) ]] 英文 English

加入行事曆加入關注加入關注已關注

Yuki Otsuka provides an overview of Lean4 and provides materials and tools to help you learn. Lean4 is an open-source theorem-proving support system and an environment that can also be used as a programming language. His presentation will not be an industrial introduction to the theorem-proving support system but will be introducing Lean4 as an environment for learning logic and mathematics through Lean4.

講者

Yuki Otsuka

Yuki Otsuka is a Japanese university student with a strong interest in open-source technologies, programming languages, programming language theory, and programming language type systems. He is a member of the Japan openSUSE user group and served as a volunteer staff member at the Linux Foundation's Open Source Summit Japan.

Open Source People Network (OSPN) Japan Special track QFRZMN general (30mins)