Recent searches
Search options
As an experiment, I asked #ChatGPT to write #Python code to compute, for each 𝑛, the length 𝑀(𝑛) of the longest subsequence of
@tao This already seems like generative AI's first killer app, right? It would make sense as there's such a huge corpus of existing, published, fact-checked code to draw from. I know Replit's AI code-writing assistant has been around for a while.
@tao Prompting can improve on this somewhat, and GPT4 exceeds GPT3.5 too - but I'm worried about copyright issues because most of its good results are close to plagiarism, which should also be an issue for academic use.
@tao Out of curiosity, how did you vet the patched produced code to ensure it does work? I always worry with code produced by these tools that the bugs can be surprisingly subtle and evade most signals we have for catching bugs
@tao I also find it interesting that you found patching it easier/faster than writing the code from scratch. I usually find the opposite is true, but maybe there are individual differences there
@TaliaRinger I don't code in Python regularly, so I do not have the basic syntax (of, say, for loops) at my fingertips (and there are some subtleties between pass-by-reference and pass-by-value that trip me up almost every time, including here when I ended up initializing a two-dimensional array incorrectly because of this, which I had to debug by manual inspection of the dynamic updates, as I mentioned previously). Having almost correct code that already has the correct syntax helps me significantly (otherwise I would have to google for almost every line of code to figure out how to phrase it exactly).
For writing a mathematical proof, which is much more in my domain expertise, I would agree with you that a GPT-provided not-quite-correct argument would not be particularly helpful for me, and it would be more efficient for me to start from scratch.
@tao you might find GitHub Copilot + VSCode useful. It has virtually eliminated the need for me to look up standard surface level syntactic structures.
@agnishom Thanks for the suggestion. I'll keep it in mind if I ever start needing to write significant amounts of code on a regular basis. For me it's more like an occasional calculation once a month or so, and each time I am tempted to find the quickest solution for that particular task rather than invest in optimizing a workflow. This is in contrast to, say, writing in LaTeX, which I do on a daily basis, and for which I have found comfortable routines already (though I would certainly welcome some AI integration into my LaTeX editor, rather than my current practice of routing random LaTeX questions through ChatGPT or Google).
@tao That makes sense. I often edit + compile my LaTeX documents from within VSCode (with LaTeX workshop + TeX live). So, Copilot is helpful there too. (Lots of repetitive syntax/equation patterns are a tab away)
@agnishom It took a while to install TeX live, but this indeed looks like a feature-rich environment for writing LaTeX. I'll try using it and see how it goes, thanks for the suggestion!
@tao That's great. I'd be interested in knowing if you eventually got GitHub Copilot to work as well.
@tao that makes sense
@tao @TaliaRinger you might want to look into #julialang - as easy to write as Python, more first-class math libraries and syntax, and easy unicode support. Math looks more like Math than most other languages.
@TaliaRinger For n=6 (the first non-trivial case due to a decrease in the totient function) I had it print out the dynamic updates and checked that it agreed with my hand implementation of the algorithm; for n up to 10 I compared the output with my hand calculations of M; and for n=10^4 I compared with the value M(10^4)=1276 that I found in the literature (at https://math.dartmouth.edu/~carlp/MonotonePhi.pdf ).
One of the authors later told me that one could use the much shorter Mathematica code
Length[LongestOrderedSequence[Table[EulerPhi[n],{n,10000}]]]
to evaluate for instance M(10000). (I then asked GPT to do the same task in Mathematica and it managed to achieve it, though not quite in such a slick one-line fashion.)
@tao this got me curious about what this looks like in a functional language like Coq. I found a cute proof development: https://github.com/taorunz/euler
And the totient looks very pretty: https://github.com/taorunz/euler/blob/master/Totient.v
But it's probably very inefficient 
nats in Coq are literally represented as 0, S 0, S S 0, ... This is probably why there are two definitions and a functional equivalence proof. I'd assume one is fast and one is pretty for proofs, a design pattern that shows up everywhere.
Totient in Lean's Mathlib also looks very beautiful: https://leanprover-community.github.io/mathlib_docs/data/nat/totient.html
@TaliaRinger @tao I assume that although the formal specification of natural numbers is unary, in most proof assistants the internal representation or extracted code still uses native integers / bignums?
@trebor @TaliaRinger @tao In Lean3, the kernel was using the unary representation but the compiler was using some usual binary representation (I can’t remember if they were native or bignums). In Lean4 both use bignums, which makes GMP part of the trusted code base.
@TaliaRinger @tao Nitpick: your last link points to the documentation for Mathlib3, the "correct" link would be https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Totient.html#Nat.totient
But of course this is not really relevant to the discussion.
@tao @yminsky Just for comparison I asked Google Bard to do it. It completely omitted the definition of varphi but on the other hand it did write something with dynamic programming in it as instructed. https://g.co/bard/share/3d9c7c07459d
@tao I’m curious how this experience compares to, say, googling for a stackoverflow or geeksforgeeks post. I asked GPT for an implementation of Gaussian elimination a few months ago; I found debugging the resulting incorrect code more difficult than writing the routine from scratch
@tao by the way, if you're interested in the first n values of Euler's totient function (like here) instead of just a given one, it is possible to compute them a lot faster by using a method based on Eratosthenes' seive: simply start with phi[i] = i, then for all primes p and multiples kp of p, multiply phi[kp] by (1-1/p). You can even use the partially computed phi to know if p is prime: it is prime if phi[p] is still equal to p when you have done the multiplications for all smaller primes.
