Zulip Chat Archive

Stream: Rutgers Lean seminar

Topic: Fall 23 project: IMO geometry

Vláďa Sedláček (Sep 27 2023 at 18:27):

A thread for formalizing IMO geometry problems. The idea is to use the API from https://github.com/ah1112/synthetic_euclid_4 and potentially also https://github.com/ianjauslin-rutgers/pythagoras4.

Notification Bot (Sep 27 2023 at 18:30):

This topic was moved here from #Rutgers Lean seminar > Project: IMO geometry by Vladimír Sedláček.

Last updated: Dec 20 2023 at 11:08 UTC