workshops:lean_workshop1224

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
workshops:lean_workshop1224 [2024/12/05 16:57] – lkastnerworkshops:lean_workshop1224 [2024/12/05 17:00] (current) – Add some project proposals lkastner
Line 49: Line 49:
 == LEAN and OSCAR == == LEAN and OSCAR ==
 OSCAR can be used to provide ingredients for proofs in LEAN, a simple example would be the inverse of a matrix. There is already some existing code that can be found at [[https://github.com/todbeibrot/Lean-Oscar|GitHub]]. We want to survey the directions we can take and sketch potential projects. OSCAR can be used to provide ingredients for proofs in LEAN, a simple example would be the inverse of a matrix. There is already some existing code that can be found at [[https://github.com/todbeibrot/Lean-Oscar|GitHub]]. We want to survey the directions we can take and sketch potential projects.
 +
 +Formation of other working groups is encouraged. Some topics have been suggested:
 +  - Polyhedral geometry in LEAN
 +  - Game theory in LEAN
 +  - [[https://www.wikidata.org/wiki/Wikidata:WikiProject_Mathematics/1000%2BTheorems]] 1000 theorems in LEAN and portal
 +  - Polynomials in LEAN
  
  
  • workshops/lean_workshop1224.1733417861.txt.gz
  • Last modified: 2024/12/05 16:57
  • by lkastner