4 ms·

I'm taking a masters in mathematics, and for me the steps are at least three-fold: understanding what you are trying to prove, which is mostly thinking about it

I'm taking a masters in mathematics, and for me the steps are at least three-fold: understanding what you are trying to prove, which is mostly thinking about it and maybe reading or talking to people; picking up pen and paper and proceeding with a sketch of the essential points; typing the proof into LaTeX for a human readable homework :) I suspect lean will change the thoughts a bit but not eliminate step one. Maybe step three becomes interactive with lean4 etc. and ends in a PR with green build, but the work does not seem likely to end there. Put it this way: Terrence Tao is unbelievably better at maths than I am; Terrence Tao with lean4 is also unbelievably better at maths than I am with lean4. As far as the value embedded in all already proven mathematics, having it in mathlib is going to make it easy to use, but extending it in the way Prof. Tao can is still pretty hard. As a side note, I've extended my experimenting with GPT4 from writing Go and emacs lisp to asking it questions about my classes and it does sound smart but will happily give fractional results for an application of Burnside's Lemma, and say things like: "An example of a simple group without an element of order 2 is any non-abelian simple group of odd order. By the Feit-Thompson theorem, every finite group of odd order is solvable, which means that non-abelian simple groups of odd order do not exist. However, this theorem does not rule out the existence of infinite simple groups of odd order." Now this answer is correct in describing how (Feit-Thompson theorem) to show that there are no simple groups of odd order, but "infinite simple groups of odd order" is pretty non-sensical. If the order is infinite, it is not odd. One hopes future iterations will develop understanding in a way that this text lacks.

t_mann 3y ago
You don't really need understanding if you ask (or train, or fine-tune) the AI to produce a formalized answer, and then write a loop that feeds back the compiler output until it's correct. That doesn't guarantee that it's the answer that you want, but it's guaranteed to be correct, so it is something. You can also use this approach to produce more training examples, if you have time you can manually check and annotate whether the result is what was originally asked for, and then hope that the training improves the accuracy of the initial answer (avoiding the loaded term 'understanding' here). This might substantially reduce the amount of work that needs to be done manually after the first step. If I was doing a Math degree right now, that's exactly the kind of stuff I'd want to do for my thesis, kind of jealous tbh.
- jhanschoo 3y ago
  This suffers from the problem of sparse rewards. You need a better reward that gives value to intermediate results or special-case answers, since too few states are correct.
  - t_mann 3y ago
    It's not about training the model. You just input the error messages together with an appropriate prompt and ask it to fix it. Iterate until it verifies successfully (or stop after you've reached ~1-2x content window length). Once you have produced examples of correct math that way, you can use those to fine-tune the model.

t_mann 3y ago

You don't really need understanding if you ask (or train, or fine-tune) the AI to produce a formalized answer, and then write a loop that feeds back the compiler output until it's correct. That doesn't guarantee that it's the answer that you want, but it's guaranteed to be correct, so it is something. You can also use this approach to produce more training examples, if you have time you can manually check and annotate whether the result is what was originally asked for, and then hope that the training improves the accuracy of the initial answer (avoiding the loaded term 'understanding' here). This might substantially reduce the amount of work that needs to be done manually after the first step. If I was doing a Math degree right now, that's exactly the kind of stuff I'd want to do for my thesis, kind of jealous tbh.

jhanschoo 3y ago
This suffers from the problem of sparse rewards. You need a better reward that gives value to intermediate results or special-case answers, since too few states are correct.
- t_mann 3y ago
  It's not about training the model. You just input the error messages together with an appropriate prompt and ask it to fix it. Iterate until it verifies successfully (or stop after you've reached ~1-2x content window length). Once you have produced examples of correct math that way, you can use those to fine-tune the model.