活動(dòng)名稱(chēng)：數(shù)學(xué)形式化簡(jiǎn)介
時(shí)間：2025年6月6日16:00
地點(diǎn)：匯賢樓數(shù)學(xué)科學(xué)學(xué)院122學(xué)術(shù)報(bào)告廳
主講人：文再文
邀請(qǐng)人：楊新民
主辦單位：數(shù)學(xué)科學(xué)學(xué)院
主講人簡(jiǎn)介：文再文，北京大學(xué)北京國(guó)際數(shù)學(xué)研究中心長(zhǎng)聘教授，北京大學(xué)博雅特聘教授，主要研究最優(yōu)化算法與理論及其在機(jī)器學(xué)習(xí)、人工智能中的應(yīng)用。2016年獲中國(guó)青年科技獎(jiǎng)。2020年獲國(guó)家萬(wàn)人計(jì)劃科技創(chuàng)新領(lǐng)軍人才，入選2023年度教育部長(zhǎng)江學(xué)者特聘教授，現(xiàn)為JSC, JORSC和CSIAM-AM等期刊編委，中國(guó)運(yùn)籌學(xué)會(huì)副理事長(zhǎng)。
活動(dòng)簡(jiǎn)介：與依賴(lài)于直覺(jué)的傳統(tǒng)數(shù)學(xué)證明方法不同，數(shù)學(xué)形式化要求每一步都經(jīng)過(guò)嚴(yán)格的論證，確保沒(méi)有任何邏輯上的漏洞或錯(cuò)誤。這種方法具有多種優(yōu)點(diǎn)：提供了對(duì)證明正確性的高度信心；已證明的定理和引理可以在其他證明中重復(fù)使用，從而鼓勵(lì)模塊化的思考方式；可以自動(dòng)化證明的某些步驟；由于每一步都明確定義，更容易看出哪里做了特定的假設(shè)或采用了哪種邏輯推理。本報(bào)告簡(jiǎn)要介紹數(shù)學(xué)形式化基礎(chǔ)知識(shí)，以及在數(shù)學(xué)優(yōu)化形式化方面的一些進(jìn)展。
