Why did an equestrian triathlon need formalized tropical algebra to avoid chaos?

When an accident disrupted an equestrian triathlon, I built a real-time rescheduling app powered by tropical algebra. To guarantee its reliability, I formalized the Max-Plus Spectral Theorem in Lean 4, bridging machine-checked mathematics with a real-world application.
Like

Share this post

Choose a social network to share with, or copy the URL to share elsewhere

This is a representation of how your post may appear on social media. The actual post will vary between social networks