I was pleasantly surprised by DeepSeek

Stream: Machine Learning for Theorem Proving

[metakuntyyy]

So a recent experience with DeepSeek was quite nice. I asked it to prove a statement of the existence of a quotient map and I for example had no idea what was needed for the context. To my big surprise it generated a completely valid proof skeleton. Everything else was broken however.

The proof skeleton itself was worth fixing though, as it compiled after an hour of tinkering. The funny thing is now that I have a compiling proof I gained much insight in what parts of the statement were crucial and which weren't. I thought that I needed an algebra homomorphism but the formalisation said a ring homomorphism is enough, which makes my life just a little bit nicer.

[metakuntyyy]

It also structured in which order I have to create the quotients, which was difficult for me to understand how to do it properly.

[Jason Rute]

Which DeepSeek model are you talking about?

[metakuntyyy]

No idea, I just used a free website. I think it was this one https://notegpt.io/chat-deepseek

[Jason Rute]

Thanks. Do you use the think button or not?

[metakuntyyy]

I don't know what you mean by think button. I just typed the query I wanted. It spit me out some lean code and I manually fixed it. Unfortunately I didn't save the query and I can't reconstruct what it spit out.

But it was something along the lines of.
Let n be a natural number, p a prime dividing it. Let m be a r-th primitive root of unity. Assume that (X^n+a)=(X+a)^n in Zn[X]/(X^r-1). Show that... or something like that

[Jason Rute]

Maybe the UI is not like this any more but it used to look like this:
image.png
In particular, there was a DeepThink button.

[Jason Rute]

Actually, the UI you mentioned (https://notegpt.io/chat-deepseek) has this also.

[metakuntyyy]

Again, I'm using notegpt, this is how it looks for me
image.png

[Jason Rute]

Yes, right there is a DeepThink (R1) button. But from context is seems you don't use it.

[metakuntyyy]

It appears not. I typed the query and pressed the enter key.

[Notification Bot]

George Tsoukalas has marked this topic as resolved.

[Notification Bot]

George Tsoukalas has marked this topic as unresolved.