Explore the challenges and opportunities in making mathematical proof more accessible through human-computer interaction design in this conference talk. Examine the current user experience of proof systems like Rocq and Lean through insights from qualitative studies of real work sessions, revealing what makes proof writing and understanding particularly difficult. Discover innovative approaches to improving proof accessibility, including tools that enhance notation comprehension and accelerate property-based testing. Learn about effective HCI research strategies for understanding the realities of proof work and evaluating the impact of new tools, with practical examples from ongoing research efforts to transform how we interact with formal proof systems.