# Zulip Chat Archive

## Stream: Machine Learning for Theorem Proving

### Topic: Galactica

#### Junyan Xu (Nov 17 2022 at 03:22):

sorry but this is hilarious :lol:

image.png

from Twitter

@ylecun @MetaAI @paperswithcode yeah... not sure this is ready yet https://twitter.com/janosch_ortmann/status/1592635890471690240/photo/1

- Janosch Ortmann (@janosch_ortmann)#### Junyan Xu (Nov 17 2022 at 03:28):

Here are some experiments I did with elliptic curves yesterday:

galactica.org

image.png image.png image.png

#### Gabriel Ebner (Nov 17 2022 at 04:38):

Clickable twitter link without the space: https://nitter.net/janosch_ortmann/status/1592635890471690240

Galactica web site: https://galactica.org/

#### Gabriel Ebner (Nov 17 2022 at 04:41):

OMG, this is hilarious:

Superposition theorem proving in Lean

This is a simple implementation of superposition in Lean, based on the SSReflect library. It can be used to prove ground theorems, given a set of ground axioms.

It is also possible to prove theorems that are universally quantified, using a ground term generator. This is not fully implemented yet.

The basic idea is that the user gives a set of axioms, and a theorem to prove, and Lean tries to find a proof using superposition. The theorem should be given in the form of an equality, since it is easier to work with, and the axioms should be equalities.

#### Floris van Doorn (Nov 17 2022 at 09:38):

:rolling_on_the_floor_laughing:

image.png

#### Johan Commelin (Nov 17 2022 at 09:47):

https://galactica.org/?prompt=Fermat%27s+Last+Theorem+in+Lean

We formalize the statement of Fermat's Last Theorem in the Lean theorem prover.

For an odd prime

`p`

, we define the statement of Fermat's Last Theorem`fermat_last_theorem p`

as follows:`variables (p : N) def fermat_last_theorem p : Prop := ∀ (a b c : N), p ∣ (a ^ p + b ^ p - c ^ p) → p ∣ a ∨ p ∣ b ∨ p ∣ c`

The

`N`

type denotes the natural numbers (`nat`

), and`p ∣ n`

denotes that`p`

divides`n`

.In this formalization, we only consider the case of

`p`

being an odd prime.

#### Johan Commelin (Nov 17 2022 at 09:50):

https://galactica.org/?prompt=Liquid+Tensor+Experiment

## Liquid Tensor Experiment

Liquid Tensor Experiment (LTE) is a video game developed by American studio Liquid Entertainment and published by Ubisoft for the Xbox 360. It was released on July 10, 2007 in North America and July 14, 2007 in Europe. It was the first Xbox 360 game to use Kinect, which is used to track the player's movements and control the game.

## Gameplay

The game features a story-based single-player mode with eight levels, each with three sections. Players use Kinect to control the protagonist, an alien named Rex, through a series of levels. Players must complete a series of objectives to advance through the level. In the first section, Rex must navigate the level using only his telekinesis. The second section involves Rex using his "tenso" abilities, which are similar to the abilities of a liquid tensor. The third section requires

#### Junyan Xu (Nov 19 2022 at 16:00):

Demo is now offline

https://twitter.com/paperswithcode/status/1593259033787600896

https://twitter.com/ylecun/status/1593293058174500865

but models still available https://github.com/paperswithcode/galai

Thank you everyone for trying the Galactica model demo. We appreciate the feedback we have received so far from the community, and have paused the demo for now. Our models are available for researchers who want to learn more about the work and reproduce results in the paper.

- Papers with Code (@paperswithcode)Galactica demo is off line for now. It's no longer possible to have some fun by casually misusing it. Happy? https://twitter.com/paperswithcode/status/1593259033787600896

- Yann LeCun (@ylecun)Last updated: Dec 20 2023 at 11:08 UTC