IPAM Research in Industrial Projects for Students (RIPS)
Jun – Aug 2026Academic mentor, Harmonic team
- Mentored an undergraduate team of 4 on an industry-sponsored formalization project. Built Lean 4 infrastructure to formalize CS algorithms and their costs in a modular way. The team produced the Lean 4 library ResourceAwareLean.