Gyde

Stream: Lean for teaching

[Alistair Tucker]

I also believe that proof verifiers can find optimal learning routes and teaching methods by assessing students. For the second belief to be realizable, a latex to formalized math converter might need to be automated, making this an important goal.

@Jony Vale Are you hoping to make a tool that can translate students’ LaTeX proofs to Lean and thereby assess their correctness? We have seen some amazing applications of LLMs in the last year or two (search e.g. LeanChat) … all the same I suspect that to aim reliably to translate proofs is a long shot at present.

[Alistair Tucker]

I guess if you only need it done very unreliably, e.g. to look for patterns in a large corpus, there might be more scope for imagination?

[Jony Vale]

Alistair Tucker said:

Are you hoping to make a tool that can translate students’ LaTeX proofs to Lean and thereby assess their correctness? We have seen some amazing applications of LLMs in the last year or two (search e.g. LeanChat) … all the same I suspect that to aim reliably to translate proofs is a long shot at present

Hi, sorry I didn’t realize the response was in Lean for Teaching. I am hoping to accelerate the the advancement of mathlib overall.

In Gyde, professors would make posts in the forms of course notes and research papers, and users would be able to reply to content and also make their own content. It would effectively be a rigorous social learning network with an emphasis on professors needs. For example, all professors currently make their own homepages, but they are all disconnected and require labor to make, moreover, these homepages are very limited in what they can do (eg. no course hosting/ Learning Management System features, nor collaborative research/ peer review or publication journals). By aggregating and organizing mathematical content, an overarching goal is to map out knowledge.

Whenever there is a post with some content (in particular, course notes from professors or research papers), the platform can encourage users to formalize the post “right there on the spot” (eg, just click a button to get an input area and start to formalize it then submit the work for review or save it to finish later, or perhaps for others to finish later). I would want the work on users end to be strictly on formalizing the mathematics, with the creating the content and submitting it for review to be a two button process. By helping in formalizing mathematics, users can gain points in Gyde which turns into solid returns as Gyde’s valuation grows (70% of Gyde will be reserved for contributing academics).

As for creating an automatic Latex to Lean converter, I figured this was ambitious and not yet feasible since I read in the article that introduced me to this community that Christian Szegedy (from Google) was working on AI systems to formalize mathematics from textbooks, but I feel that such a goal would be eventually achievable in a company like the one I imagine.

All though I view it as important goal, I don’t view it as an immediate goal because

1. There is much more that needs to be done that can certainly be done (a quote I got while in India was 38.5 months).
2. We can begin to contribute to mathlib by encouraging human users to formalize math on the education platform

[Jony Vale]

Alistair Tucker said:

I guess if you only need it done very unreliably, e.g. to look for patterns in a large corpus, there might be more scope for imagination?

In response to your second message, the thought intrigues me. Do you think if current technology can convert math to lean poorly, that this would still help accelerate human effort?

For example, instead of writing an entire definition or piece of math in Lean, a human can receive the poorly written formalization created by Lean, and they can fix the errors and add missing pieces

I don’t know how effective this would be, but I have to imagine that this could save users time as the converters, and if AI systems are analyzing these corrections, I imagine the converters only getting better

[Scott Morrison]

Everyone interested in this question should make sure to look at #3808, the #formalize PR for Mathlib. I doubt we're going to merge it, but it's interesting to play with it nonetheless. GPT-4 API key needed for best effect, but there is a pluggable architecture for LLMs so if anyone wants to add others, please do.

[Alistair Tucker]

In response to your second message, the thought intrigues me. Do you think if current technology can convert math to lean poorly, that this would still help accelerate human effort?

On this your guess is as good as mine! I was rather speaking in the context of your initially stated goal to "find optimal learning routes and teaching methods by assessing students" by what I assumed would be some sort of automated/ML procedure.

Sorry if it was unhelpful to start this new topic in "Lean for Teaching"! My logic was that people subscribed to "job postings" are unlikely to care much for my witterings. But they may well be interested in the longer description of your vision that you have now provided—so maybe you'd be wise to copy that back to the original stream?

[Jony Vale]

Alistair Tucker said:

I was rather speaking in the context of your initially stated goal to "find optimal learning routes and teaching methods by assessing students" by what I assumed would be some sort of automated/ML procedure.

You are correct in assuming I do seek an ML procedure to automate the conversion between Latex, (and since Textbook to Latex is doable too) and images of math, directly into Lean! I simply don't believe it is possible nor practical to prioritize this. Nonetheless, I would love to have as a cofounder a programming guru that knows Lean, simply to ensure that the platform is created to be friendly to Lean-- for example, by ensuring that users can easily type in Lean to formalize mathematics in the platform.

Also, I totally see your logic and personally also agree that this seems more like a topic about educating people about what Lean can and can't do, and so it seems fitting to put it in Lean for Teaching. I simply was confused since I'm knew the platform. I saw a notification that a response was moved, but didn't know it was a response to my post. Thank you for sharing your insights and helping to organize the content in Zulip (/mathlib)!