### Run All Instructions

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Execute all setup and installation steps in a single command. Ensure you are in the project's root directory.

```bash
bash run.sh
```

--------------------------------

### Install Dependencies and Activate Virtual Environment

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Sets up a Python virtual environment and installs project dependencies from requirements.txt. This is a prerequisite for running the solver.

```bash
virtualenv -p python3 .
source ./bin/activate
pip install --require-hashes -r requirements.txt
```

--------------------------------

### Install Meliad Library

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Manually installs the 'meliad' library, which is not available via pip. This involves cloning the repository and setting the PYTHONPATH environment variable.

```bash
MELIAD_PATH=meliad_lib/meliad
mkdir -p $MELIAD_PATH
git clone https://github.com/google-research/meliad $MELIAD_PATH
export PYTHONPATH=$PYTHONPATH:$MELIAD_PATH
```

--------------------------------

### DDAR Solver Output Example

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Example output from the DDAR solver, showing the geometric predicates derived and the step-by-step proof construction. Predicates are numbered for traceability.

```log
graph.py:468] translated_imo_2000_p1
graph.py:469] a b = segment a b; g1 = on_tline g1 a a b; g2 = on_tline g2 b b a; m = on_circle m g1 a, on_circle m g2 b; n = on_circle n g1 a, on_circle n g2 b; c = on_pline c m a b, on_circle c g1 a; d = on_pline d m a b, on_circle d g2 b; e = on_line e a c, on_line e b d; p = on_line p a n, on_line p c d; q = on_line q b n, on_line q c d ? cong e p e q
ddar.py:41] Depth 1/1000 time = 1.7772269248962402
ddar.py:41] Depth 2/1000 time = 5.63526177406311
ddar.py:41] Depth 3/1000 time = 6.883412837982178
ddar.py:41] Depth 4/1000 time = 10.275688409805298
ddar.py:41] Depth 5/1000 time = 12.048273086547852
alphageometry.py:190]
==========================
 * From theorem premises:
A B G1 G2 M N C D E P Q : Points
AG_1 ⟂ AB [00]
BA ⟂ G_2B [01]
G_2M = G_2B [02]
G_1M = G_1A [03]

... [log omitted] ...

036. ∠QEB = ∠(QP-EA) [46] & ∠(BE-QP) = ∠AEP [55] ⇒  ∠EQP = ∠QPE [56]
037. ∠PQE = ∠EPQ [56] ⇒  EP = EQ
==========================
```

--------------------------------

### Run Test Suite

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Execute the test suite to ensure proper setup before reproducing paper results. This script verifies the integrity of the AlphaGeometry installation.

```bash
run_tests.sh
```

--------------------------------

### Define Proof Search Flags

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Set lightweight values for proof search parameters like batch size, beam size, and search depth for simple examples.

```shell
BATCH_SIZE=2
BEAM_SIZE=2
DEPTH=2

SEARCH_ARGS=(
  --beam_size=$BEAM_SIZE
  --search_depth=$DEPTH
)
```

--------------------------------

### AlphaGeometry Output Example

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

This output illustrates the execution flow of AlphaGeometry, including parameter counts, task creation, problem definition, DDAR progress, LM proposals for auxiliary constructions, and the final proof steps.

```text
... [log omitted] ...
training_loop.py:725] Total parameters: 152072288
training_loop.py:739] Total state size: 0
training_loop.py:492] Training loop: creating task for mode beam_search

graph.py:468] orthocenter
graph.py:469] a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b ? perp a d b c
ddar.py:41] Depth 1/1000 time = 0.009987592697143555 branch = 4
ddar.py:41] Depth 2/1000 time = 0.00672602653503418 branch = 0
alphageometry.py:221] DD+AR failed to solve the problem.
alphageometry.py:457] Depth 0. There are 1 nodes to expand:
alphageometry.py:460] {S} a : ; b : ; c : ; d : T a b c d 00 T a c b d 01 ? T a d b c {F1} x00
alphageometry.py:465] Decoding from {S} a : ; b : ; c : ; d : T a b c d 00 T a c b d 01 ? T a d b c {F1} x00
... [log omitted] ...
alphageometry.py:470] LM output (score=-1.102287): "e : C a c e 02 C b d e 03 ;"
alphageometry.py:471] Translation: "e = on_line e a c, on_line e b d"

alphageometry.py:480] Solving: "a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b; e = on_line e a c, on_line e b d ? perp a d b c"
graph.py:468]
graph.py:469] a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b; e = on_line e a c, on_line e b d ? perp a d b c
ddar.py:41] Depth 1/1000 time = 0.021120786666870117
ddar.py:41] Depth 2/1000 time = 0.033370018005371094
ddar.py:41] Depth 3/1000 time = 0.04297471046447754
alphageometry.py:140]
==========================
 * From theorem premises:
A B C D : Points
BD ⟂ AC [00]
CD ⟂ AB [01]

 * Auxiliary Constructions:
E : Points
E,B,D are collinear [02]
E,C,A are collinear [03]

 * Proof steps:
001. E,B,D are collinear [02] & E,C,A are collinear [03] & BD ⟂ AC [00] ⇒  ∠BEA = ∠CED [04]
002. E,B,D are collinear [02] & E,C,A are collinear [03] & BD ⟂ AC [00] ⇒  ∠BEC = ∠AED [05]
003. A,E,C are collinear [03] & E,B,D are collinear [02] & AC ⟂ BD [00] ⇒  EC ⟂ EB [06]
004. EC ⟂ EB [06] & CD ⟂ AB [01] ⇒  ∠(EC-BA) = ∠(EB-CD) [07]
005. E,C,A are collinear [03] & E,B,D are collinear [02] & ∠(EC-BA) = ∠(EB-CD) [07] ⇒  ∠BAE = ∠CDE [08]
006. ∠BEA = ∠CED [04] & ∠BAE = ∠CDE [08] (Similar Triangles)⇒  EB:EC = EA:ED [09]
007. EB:EC = EA:ED [09] & ∠BEC = ∠AED [05] (Similar Triangles)⇒  ∠BCE = ∠ADE [10]
008. EB:EC = EA:ED [09] & ∠BEC = ∠AED [05] (Similar Triangles)⇒  ∠EBC = ∠EAD [11]
009. ∠BCE = ∠ADE [10] & E,C,A are collinear [03] & E,B,D are collinear [02] & ∠EBC = ∠EAD [11] ⇒  AD ⟂ BC
==========================

alphageometry.py:505] Solved.
```

--------------------------------

### Execute README Instructions

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Script to execute instructions as detailed in the README file.

```bash
run.sh
```

--------------------------------

### Set up Symbolic Engine Flags

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Define flags for the symbolic engine, specifying the paths to definition and rule files.

```shell
DDAR_ARGS=(
  --defs_file=$(pwd)/defs.txt \
  --rules_file=$(pwd)/rules.txt \
);
```

--------------------------------

### Download Model Weights and Vocabulary

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Downloads pre-trained model weights and vocabulary files necessary for the AlphaGeometry solver. The DATA variable should be set to the downloaded checkpoint directory.

```bash
bash download.sh
DATA=ag_ckpt_vocab
```

--------------------------------

### Download Checkpoints and LM

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Script to download necessary model checkpoints and language models for AlphaGeometry.

```bash
download.sh
```

--------------------------------

### Configure Language Model Flags

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Define flags for the language model, including checkpoint and vocabulary paths, gin search paths, and gin configuration files. Parameters for model configuration, batch size, sequence length, and state restoration are also set.

```shell
LM_ARGS=(
  --ckpt_path=$DATA \
  --vocab_path=$DATA/geometry.757.model
  --gin_search_paths=$MELIAD_PATH/transformer/configs,$(pwd) \
  --gin_file=base_htrans.gin \
  --gin_file=size/medium_150M.gin \
  --gin_file=options/positions_t5.gin \
  --gin_file=options/lr_cosine_decay.gin \
  --gin_file=options/seq_1024_nocache.gin \
  --gin_file=geometry_150M_generate.gin \
  --gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True \
  --gin_param=TransformerTaskConfig.batch_size=$BATCH_SIZE \
  --gin_param=TransformerTaskConfig.sequence_length=128 \
  --gin_param=Trainer.restore_state_variables=False
);
```

--------------------------------

### Run DDAR Solver for IMO 2000 P1

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Execute the DDAR solver for a specific problem from a problems file. Use `--mode=ddar` to specify the solver and provide the problem file and name via flags. Additional arguments can be passed via `DDAR_ARGS`.

```shell
python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/imo_ag_30.txt \
--problem_name=translated_imo_2000_p1 \
--mode=ddar \
"${DDAR_ARGS[@]}"
```

--------------------------------

### Run AlphaGeometry Solver

Source: https://github.com/google-deepmind/alphageometry/blob/main/README.md

Execute AlphaGeometry with specified problem files, mode, and arguments. Ensure DDAR_ARGS, SEARCH_ARGS, and LM_ARGS are properly defined before running.

```shell
python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/examples.txt \
--problem_name=orthocenter \
--mode=alphageometry \
"${DDAR_ARGS[@]}" \
"${SEARCH_ARGS[@]}" \
"${LM_ARGS[@]}"
```

--------------------------------

### Equal Angle Construction with Lines and Circles

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a configuration with equal angles using points on lines and circles. Defines feet of perpendiculars and points on lines/circles to establish angle equality.

```AlphaGeometry
b c r = triangle b c r; o = circle o b c r; s = on_circle s o b; a = on_line a b r, on_line a c s; m = foot m a r s; n = foot n a b c ? eqangle a b a m a n a c
```

--------------------------------

### Parallel Line Construction with Free Point

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a parallel line using a free point and circles. Defines points on circles and lines to establish parallelism.

```AlphaGeometry
a b c = triangle a b c; f = free f; p = circle p a b f; o = circle o a b c; e = on_circle e p a, on_line e a c; d = on_circle d o b, on_line d b f ? para c d e f
```

--------------------------------

### Equal Angle Construction with Feet

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a configuration with equal angles using feet of perpendiculars and points on circles and lines.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; p = foot p o a c; q = foot q o a b; m = on_line m o q, on_circle m o a; n = on_line n o p, on_circle n o a; e = on_line e a c, on_line e n m; d = on_line d a b, on_line d n m ? eqangle d a d e e d e a
```

--------------------------------

### Equal Angle Construction with Intersecting Circles

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a configuration with equal angles using intersecting circles and lines. Defines points on circles and lines to establish the angle equality.

```AlphaGeometry
q r p = triangle q r p; o1 = circle o1 q r p; s = on_circle s o1 q; y = on_line y q s; o = circle o y p q; x = on_circle x o q; i = on_line i r s, on_line i y x ? eqangle i r i x p r p x
```

--------------------------------

### Cyclic Quadrilateral with Mirror

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a cyclic quadrilateral using mirror images and points on lines. Defines feet of perpendiculars and mirror points to establish the cyclic property.

```AlphaGeometry
o x l = triangle o x l; a = foot a l o x; y = free y; b = foot b l o y; p = mirror p l a; q = mirror q l b; q1 = on_line q1 l a, on_line q1 o y; p1 = on_line p1 o x, on_line p1 l b ? cyclic o p q p1
```

--------------------------------

### Cyclic Quadrilateral with Feet

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a cyclic quadrilateral using feet of perpendiculars from a point on a circle to the sides of a triangle.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; d = on_circle d o a; p = on_circle p o a; f = foot f p a d; g = foot g p a b; h = foot h p b c; e = foot e p c d; i = on_line i f g, on_line i h e ? cyclic p g i h
```

--------------------------------

### Triangle Excenter Construction

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Constructs the excenters of a triangle and defines points on lines related to these excenters. Used to check congruence of segments.

```AlphaGeometry
a b c = triangle a b c; m l k j = excenter2 m l k j a b c; f = on_line f m l, on_line f b j; g = on_line g m k, on_line g c j; s = on_line s f a, on_line s b c; t = on_line t g a, on_line t c b ? cong m s m t
```

--------------------------------

### Cyclic Quadrilateral Construction

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a cyclic quadrilateral given a triangle and its circumcircle. Defines points on lines and circles to establish the cyclic property.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; h = midpoint h c b; d = on_line d o h, on_line d a b; e = on_tline e c c o, on_tline e a a o ? cyclic a o e d
```

--------------------------------

### Perpendicular Line Construction with Feet

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a perpendicular line using feet of perpendiculars from points on lines to sides of a triangle.

```AlphaGeometry
a b o = triangle a b o; m = on_line m a b; p = foot p m a o; q = foot q m b o; d = foot d b a o; c = foot c a b o; t = foot t q a o; k = foot k p b o; s = on_line s q t, on_line s p k ? perp o s p q
```

--------------------------------

### Congruent Segment Construction with Midpoints

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs congruent segments using midpoints and lines. Defines points on lines and midpoints to establish congruence.

```AlphaGeometry
a b c = triangle a b c; p = midpoint p b a; q = midpoint q c b; d = on_tline d b a c; r = midpoint r d c; s = midpoint s a d; o = on_line o p r, on_line o q s ? cong o s o r
```

--------------------------------

### Mirror Transformation and Congruence

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle, uses mirror transformations on points, and constructs lines and circles. Used to check for congruence of circles.

```AlphaGeometry
a b c = triangle a b c; p = on_line p b c, on_aline p a b b c a; q = on_line q b c, on_aline q a c c b a; m = mirror m a p; n = mirror n a q; x = on_line x b m, on_line x c n; o = circle o a b c ? cong o x o a
```

--------------------------------

### Cyclic Quadrilateral with Feet of Perpendiculars

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a cyclic quadrilateral by defining points as feet of perpendiculars from a point on a circle to the sides of a triangle.

```AlphaGeometry
a b c = triangle a b c; g = foot g c a b; o = circle o a b c; d = on_circle d o c, on_line d c g; e = foot e d a c; f = foot f d b c ? cyclic a e f b
```

--------------------------------

### Equal Angle Construction

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a configuration where two angles are equal. Involves midpoints, circles, and points on lines and circles.

```AlphaGeometry
a b c = triangle a b c; m = midpoint m b a; o = circle o a b c; n = on_line n o m, on_circle n o a ? eqangle c a c n c n c b
```

--------------------------------

### Congruent Segment Construction with Right Triangle and Lines

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs congruent segments within a right triangle using points on lines and circles.

```AlphaGeometry
e c d = r_triangle e c d; o = midpoint o d c; a = on_tline a c c d, on_tline a e e o; f = on_line f c a, on_line f d e ? cong a e a f
```

--------------------------------

### Triangle, Angle Bisectors, and Congruence

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle and its angle bisectors, then constructs points on lines and alines. Used to check for congruence of lengths.

```AlphaGeometry
p a b = triangle p a b; x = angle_bisector p b a; y = angle_bisector p a b; z = on_aline z a p a b x; t = on_aline t p a p a z; d = on_aline d p t p b a, on_line a z; u = on_aline u b p b a y; v = on_aline v p b p b u; c = on_aline c p v p a b, on_line b u; o = angle_bisector a d p, angle_bisector p c b ? cong o a o b
```

--------------------------------

### Perpendicular Line Construction with Midpoint

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a perpendicular line using a triangle, midpoint, and circle. Defines points on lines and circles to establish perpendicularity.

```AlphaGeometry
p a b = triangle p a b; o = midpoint o b a; a1 = on_line a1 p a, on_circle a1 o a; b1 = on_line b1 p b, on_circle b1 o a; o1 = circle o1 p a1 b1 ? perp o a1 a1 o1
```

--------------------------------

### Triangle, Lines, and Cyclic Quadrilateral

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle and points on lines, then uses angle equality to define new points. Used to check if four points are concyclic.

```AlphaGeometry
a b c = triangle; a1 = on_line b c; b1 = on_line a c; p = on_line a a1; q = on_line b b1, on_pline p a b; p1 = on_line p b1, eqangle3 p c a b c; q1 = on_line q a1, eqangle3 c q b c a ? cyclic p q p1 q1
```

--------------------------------

### Parallel Line Construction

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a line parallel to a given line segment. Utilizes circles, feet of perpendiculars, and points on lines to establish parallelism.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; d = on_circle d o a; g = foot g d a b; f = foot f d a c; c1 = on_circle c1 o d, on_line c1 d g; b1 = on_circle b1 o d, on_line b1 d f ? para c1 c b1 b
```

--------------------------------

### Congruent Segment Construction with Tangent and Intersection

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs congruent segments using tangent lines and intersections of circles and lines.

```AlphaGeometry
a o = segment a o; b = on_circle b o a; c = on_line c a b; e = intersection_tt e b b o c c o; d = intersection_lt d c e a a o ? cong o e o d
```

--------------------------------

### Segment, Distance, Angle, and Cyclic Quadrilateral

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a segment, constructs points with equal distance and angle properties, and checks for a cyclic quadrilateral.

```AlphaGeometry
b c = segment; d = free; e = eqdistance d b c; t = on_bline b d, on_bline c e; a = eqangle2 b t e; p = on_line a b, on_line c d; q = on_line a b, on_line c t; r = on_line a e, on_line c d; s = on_line a e, on_line d t ? cyclic p q r s
```

--------------------------------

### Perpendicular Line Construction with Incenter

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a perpendicular line using the incenter of a triangle and circumcenter. Defines points on lines and circles to establish perpendicularity.

```AlphaGeometry
m b c = triangle m b c; i = incenter i m b c; i_b = on_tline i_b c c i, on_line i_b b i; i_c = on_tline i_c b b i, on_line i_c c i; a = midpoint a i_b i_c; o = circumcenter o b i c ? perp a b b o
```

--------------------------------

### Congruent Segment Construction with Tangents

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs congruent segments using tangents to circles and intersections. Defines points on circles and intersections to establish congruence.

```AlphaGeometry
o a = segment o a; p = on_circle p a o; q = intersection_cc q a o p; r = lc_tangent r p a, on_circle r o p ? cong p q p r
```

--------------------------------

### Congruent Segment Construction with Isosceles Triangle

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs congruent segments within an isosceles triangle. Uses lines, circles, and points on lines/circles to establish congruence.

```AlphaGeometry
m a b = iso_triangle m a b; o = circle o a b m; d = on_line d m o, on_line d a b; e = on_tline e a a o, on_pline e m a o ? cong m e m d
```

--------------------------------

### Angle Bisector and Parallelogram

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Constructs angle bisectors and points on lines, then forms a parallelogram. Used to check for collinearity of points.

```AlphaGeometry
a b z = triangle a b z; f = angle_bisector f b a z, on_bline f a b; c = on_tline c b f b, on_line c a f; d = on_line d a z, on_bline d a c; e = angle_mirror e c a d, on_bline e a d; m = midpoint m c f; x = parallelogram e a m x; y = on_line y f x, on_line y e m ? coll y b d
```

--------------------------------

### Congruent Segment Construction with Right Triangle

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs congruent segments within a right triangle. Uses feet of perpendiculars, midpoints, and lines to define points and establish congruence.

```AlphaGeometry
a b c = r_triangle a b c; d = foot d a b c; o = midpoint o c b; m = foot m b a o; g = on_line g b m, on_circle g o a; f = on_line f c a, on_line f b m; e = on_line e a d, on_line e b m ? cong e a e b
```

--------------------------------

### Orthocenter, Midpoint, and Circles

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Constructs the orthocenter and midpoint of a triangle's side, then defines circles and points on them. Used to check for collinearity of circle centers.

```AlphaGeometry
a b c = triangle a b c; h = orthocenter h a b c; f = on_line f h a, on_line f b c; m = midpoint m b c; o = circle o a b c; q = on_dia q a h, on_circle q o a; k = on_dia k h q, on_circle k o a; o1 = circle o1 k q h; o2 = circle o2 f k m ? coll o1 o2 k
```

--------------------------------

### Triangle, Circles, and Parallelogram

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle, its circumcircle, and points on lines and circles. Used to check if four points form a parallelogram.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; d = on_line d a b; e = on_line e a c, on_circle e a d; f = on_bline f b d, on_circle f o a; g = on_bline g e c, on_circle g o a ? para d e f g
```

--------------------------------

### Mirror, Circle, and Perpendicularity

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a segment, its mirror, and points on lines and circles. Used to check for perpendicularity between lines.

```AlphaGeometry
r s = segment r s; t = mirror t r s; o = on_bline o r s; j = on_circle j o s; o1 = circle o1 j s t; a = on_tline a r o r, on_circle a o1 s; b = on_tline b r o r, on_circle b o1 s; k = on_line k j a, on_circle k o s ? perp k t o1 t
```

--------------------------------

### Triangle with Foot and Circle

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle, its orthic triangle, and points on lines and circles. Used to check congruence of segments.

```AlphaGeometry
c a b = r_triangle c a b; d = foot d c a b; x = on_line x c d; k = on_line k a x, on_circle k b c; l = on_line l b x, on_circle l a c; m = on_line m a l, on_line m b k ? cong m k m l
```

--------------------------------

### Orthocenter and Circles

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Constructs the orthocenter of a triangle and defines points on lines and circles related to it. Used to check for collinearity of points.

```AlphaGeometry
a b c = triangle a b c; h = orthocenter h a b c; m = on_line m h b, on_line m a c; n = on_line n h c, on_line n a b; w = on_line w b c; o1 = circle o1 b n w; o2 = circle o2 c m w; x = on_line x o1 w, on_circle x o1 w; y = on_line y o2 w, on_circle y o2 w ? coll x h y
```

--------------------------------

### Congruent Segment Construction

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs congruent segments using the orthocenter and circumcircle. Defines points on circles and lines to establish congruence.

```AlphaGeometry
a b c = triangle a b c; h = orthocenter h a b c; o = circle o a b c; c1 = on_circle c1 o c, on_line c1 c h; a1 = on_circle a1 o a, on_line a1 a h ? cong b a1 b c1
```

--------------------------------

### Circle Intersections and Tangents

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle and its circumcircle, then constructs points on lines and circles. Used to check for collinearity of points.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; d = on_line d b c; e = on_line e b c, on_circle e a d; f = on_circle f o a, on_circle f a d; g = on_circle g o a, on_circle g a d; o1 = circle o1 f b d; o2 = circle o2 g c e; k = on_circle k o1 b, on_line k a b; l = on_circle l o2 c, on_line l a c; x = on_line x f k, on_line x l g ? coll x o a
```

--------------------------------

### Perpendicular Line Construction

Source: https://github.com/google-deepmind/alphageometry/blob/main/jgex_ag_231.txt

Constructs a line perpendicular to another line segment. Uses midpoints and feet of perpendiculars to define points and relationships.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; d = on_circle d o a; q = midpoint q c b; s = midpoint s a d; j = midpoint j s q; m = mirror m o j; i = on_line i a d, on_line i b c ? perp s m b c
```

--------------------------------

### Incenter, Circles, and Perpendicularity

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Constructs the incenter of a triangle and defines points on lines and circles. Used to check for perpendicularity between a line and a point.

```AlphaGeometry
a b c = triangle a b c; d e f i = incenter2 d e f i a b c; r = on_tline r d e f, on_circle r i d; p = on_line p r a, on_circle p i d; o1 = circle o1 p c e; o2 = circle o2 p b f; q = on_circle q o1 p, on_circle q o2 p; t = on_line t p q, on_line t i d ? perp a t a i
```

--------------------------------

### Angle Bisector and Collinearity

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle, its angle bisector, and points on lines and circles. Used to check for collinearity of points.

```AlphaGeometry
a b c = triangle; d = angle_bisector b a c; e = on_aline d a d c b, on_line a c; f = on_aline d a d b c, on_line a b; x = on_bline b c, on_line a c; o1 = circle a d c; o2 = circle e x d; y = on_line e f, on_line b c ? coll o1 o2 y
```

--------------------------------

### Triangle and Circle Intersection

Source: https://github.com/google-deepmind/alphageometry/blob/main/imo_ag_30.txt

Defines a triangle and a circle passing through its vertices, then finds a point that lies on both the original circle and a new circle defined by transformed points. Used for collinearity checks.

```AlphaGeometry
a b c = triangle a b c; o = circle o a b c; p = on_circle p o a; q = on_tline q p o p; pa = reflect pa p b c; pb = reflect pb p c a; pc = reflect pc p a b; qa = reflect qa q b c; qb = reflect qb q c a; qc = reflect qc q a b; a1 = on_line a1 pb qb, on_line a1 pc qc; b1 = on_line b1 pa qa, on_line b1 pc qc; c1 = on_line c1 pa qa, on_line c1 pb qb; o1 = circle o1 a1 b1 c1; x = on_circle x o a, on_circle x o1 a1 ? coll x o o1
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.