Tuesday, December 23, 2025

<< >>  
2025. 11
Sun Mon Tue Wed Thu Fri Sat
1
2 3 4 5 6 7 8
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30
2025. 12
Sun Mon Tue Wed Thu Fri Sat
1 2 3 4 5 6
7 8 9 10 11 12 13
14 15 16 17 18 19 20
21 22 23 24 25 26 27
28 29 30 31
2026. 1
Sun Mon Tue Wed Thu Fri Sat
1 2 3
4 5 6 7 8 9 10
11 12 13 14 15 16 17
18 19 20 21 22 23 24
25 26 27 28 29 30 31
2025-12-26 / 10:00 ~ 11:30
AI수학대학원 - AI수학대학원 세미나: 인쇄
by 현지훈()
Interactive theorem provers (ITPs) are becoming crucial in mathematics, supporting the development of fully verified proofs and mathematically rigorous infrastructure. Their importance comes not only from catching mistakes that humans overlook, but also from enabling large-scale formalization projects that would be impossible to manage manually. In this talk, I will give an accessible overview of formalizing mathematics in Lean4 and outline how its underlying theory and tooling support modern proof development. In advance, I will present several mathematical projects that showcase the strengths of ITPs.
2025-12-26 / 16:30 ~ 17:30
IBS-KAIST 세미나 - 이산수학: Grassmann-Plücker functions for orthogonal matroids 인쇄
by Donggyu Kim(Georgia Institute of Technology)
We present a new cryptomorphic definition of orthogonal matroids with coefficients using Grassmann-Plücker functions. The equivalence is motivated by Cayley’s identities expressing principal and almost-principal minors of a skew-symmetric matrix in terms of its pfaffians. As a corollary of the new cryptomorphism, we deduce that each component of the orthogonal Grassmannian is parameterized by certain part of the Plücker coordinates. This is joint work with Changxin Ding.
2025-12-30 / 16:30 ~ 17:30
IBS-KAIST 세미나 - 이산수학: Sampling and volume computation 인쇄
by 국윤범(Georgia Institute of Technology)
Since the development of the first randomized polynomial-time algorithm for volume computation by Dyer, Frieze, and Kannan in 1989, convex-body sampling has been a central problem at the intersection of algorithms, geometry, and probability. A major milestone came in 1997, when Kannan, Lovász, and Simonovits analyzed the Ball Walk and formulated the influential KLS conjecture. This was extended to log-concave distributions by Lovász and Vempala in 2006, and further accelerated by Cousins and Vempala in 2015 through warm-start generation techniques. In this talk, I will present a gentle introduction to these milestones and how they have been streamlined and improved in the past few years. The talk is based on joint work with Santosh Vempala.
Events for the 취소된 행사 포함 모두인쇄
export to Google calendar  .ics download