Bharat Rakshak

Just to be complete, teorth is Terence Tao's ghithub page.

https://github.com/teorth

https://google-deepmind.github.io/forma ... s/397.html

The formal definition of eRDOS #397 is above. It is machine-readable, I suppose. Never mind. It is a Lean description of the problem. I am more familiar with HOL Light (which is written in Ocaml). I learnt Ocaml to follow some of the proofs in the HOL Light database. I found that syntax to be natural. Currently, Lean and Rocq (previously Coq) offer all the features and are the most popular.

Terence Tao made a post on Mathsodon on how LLMs can be useful in theorem proving (the end goal is to have a full-fledged automatic theorem provers - ATPs for short) using Interactive Theorem Provers, AKA Proof Assistants, coupled with LLMs. The important and key difference between ITPs and ATPs is that an ITP requires a human to guide it to prove/disprove a conjecture, whereas an ATP can prove/disprove a conjecture on its own.

jatin
@jatinkrmalik
·
Jan 9
The reason why RAM has become four times more expensive is that a huge amount of RAM that has not yet been produced was purchased with non-existent money to be installed in GPUs that also have not yet been produced, in order to place them in data centers that have not yet been built, powered by infrastructure that may never appear, to satisfy demand that does not actually exist and to obtain profit that is mathematically impossible.

https://x.com/jatinkrmalik/status/20096 ... 18887?s=20

Also, jatin posted a graphic of the same.

For those who like to test or play with their favorite AI, there are a few problems in the math thread—you can use them to see how the AI approaches and solves them.