Tim Shephard - Quick Intro

Stream: new members

[Deleted User 968128]

Just a little bit about myself.

While new to lean and with 4th year math at most, I was a Director of Engineering at Oracle and have a reasonably storied career in software. For the last few years I have spent a quite a bit of time in ML and LLMs (top 1% on AI Competitions).

Recently, I've noticed a few misconceptions that have appeared in math papers around LLMs and postings in social media from math experts. They aren't fundamental misconceptions, but enough that I believe some important people are working at a disadvantage and wanted to help in anyway that I can.

In short, my goal here is to help ensure that folks in the lean community have a baseline understanding of LLMs/AI and ML and their capabilities to accelerate auto-formalization efforts around lean.

[(deleted)]

I've always been supportive of AI when it actually works. And I hope you'll get better at Lean.

[Kenny Lau]

What are those misconceptions?

[(deleted)]

#Machine Learning for Theorem Proving > Math, Inc, and Gauss discussion @ 💬

[(deleted)]

This is one of the misconceptions that Tim has corrected

[Deleted User 968128]

Kenny Lau said:

What are those misconceptions?

Nothing serious for sure, but it occurred to me that the focus, expertise and interest is in math rather than software and some knowledge transfer might help as it becomes more relevant to the field.

Indeed, on zulip here the level of knowledge is far ahead of what I see elsewhere. I am sure my contributions will be minimal at most.

[Deleted User 968128]

I am also hoping I won't be the only one with a similar background that will be jumping in to assist where they can.