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