Using lean is a verifier for high school level geometry

Stream: mathlib4

[eitan]

(deleted)

[eitan]

(deleted)

[eitan]

A question that is more General and for a beginner for the work with Lean- if I'm trying to solve foundational High School level geometry problems in Lean. I'm trying to build a verifier with lean that's given a High School level geometry problem and a solution like -
DESCRIPTION:

As shown in the diagram, ∠WZY=a+2°, ∠XWZ=a/2+8°, ∠YXW=a°, ∠ZYX=a-28°. Find the measure of ∠ZYX.

CONSTRUCTION_CDL:

Shape(XW,WZ,ZY,YX)

TEXT_CDL:

Equal(MeasureOfAngle(WZY),a+2)

Equal(MeasureOfAngle(XWZ),a/2+8)

Equal(MeasureOfAngle(YXW),a)

Equal(MeasureOfAngle(ZYX),a-28)

GOAL_CDL:

Value(MeasureOfAngle(ZYX))

CONSTRUCTION_CDL_EXTENDED:

Shape(WZ,ZY,YX,XW)

Shape(ZY,YX,XW,WZ)

Shape(YX,XW,WZ,ZY)

Point(X)

Point(W)

Point(Z)

Point(Y)

Line(XW)

Line(WX)

Line(WZ)

Line(ZW)

Line(ZY)

Line(YZ)

Line(YX)

Line(XY)

Angle(XWZ)

Angle(WZY)

Angle(ZYX)

Angle(YXW)

Angle(ZWX)

Angle(YZW)

Angle(XYZ)

Angle(WXY)

Polygon(XWZY)

Polygon(WZYX)

Polygon(ZYXW)

Polygon(YXWZ)

SYMBOLS_AND_VALUES:

LengthOfLine(AD);ll_ad;None

LengthOfLine(DA);ll_ad;None

LengthOfLine(BC);ll_bc;None

LengthOfLine(CB);ll_bc;None

MeasureOfAngle(DCB);ma_dcb;101

MeasureOfAngle(ADC);ma_adc;None

EQUATIONS:
-a+ma_wzy=2
-a/2+ma_xwz=8
-a+ma_yxw=0
-a+ma_zyx+28=0

GOAL_SYMBOL:

ma_zyx

ANSWER:

80

THEOREM_SEQUENCE:

step_id: 1; theorem: quadrilateral_property_angle_sum(1,XWZY); premise: Polygon(XWZY); conclusion: ["Equal(Add(MeasureOfAngle(XWZ),MeasureOfAngle(WZY),MeasureOfAngle(ZYX),MeasureOfAngle(YXW)),360)"]

Picture1.png

Can I use mathlib4 with lean in some way to go over the steps and to check if the theorem are correct?
To ask more precisely- are all the basic level geometric Theorem are already implemented in lean4?

[eitan]

(deleted)

[eitan]

(deleted)

[Jireh Loreaux]

Please don't post in multiple channels. Pick only the correct channel and use only a single thread.

[eitan]

I'm sorry I'm new here, I dont see an option to delete the message

[Jireh Loreaux]

If you just edit the message so that it's empty, it will appear as "(deleted)", but also you can just post a message in each thread saying that they are duplicates and linking to the thread where you want discussion to take place.

[Eric Wieser]

I've moved all the deleted comments to here to avoid confusion

[Eric Wieser]

(it's possible you didn't have the power to do this yourself @eitan)

[Ilmārs Cīrulis]

There are some results from Euclidean geometry in Mathlib, but not much as far as I understand.

[Ilmārs Cīrulis]

I don't understand what that long text exactly means, but that looks like some kind of DSL (Domain Specific Language) or something like that. (But I'm sleepy.)

Even if there were are high-school geometry inside Mathlib, it still wouldn't be easy (at least for beginner?) to make Lean program that verifies such proofs (?) from high-school geometry.

My two cents.

[eitan]

@Lessness
Thank you so much for your response!
You did get right what I'm trying to do. Is Mathlib the only relevant library to find such a thing?

[Ilmārs Cīrulis]

Mathlib is the biggest I know. Maybe there's something for Euclidean geometry made by some third party, but then I don't know about it.

[Ilmārs Cīrulis]

Out of curiosity - what's the text you have pasted in in your first post. What's the software etc?

[eitan]

It's a University project I'm working on I got it from an NLP dataset (I'm not sure which, I'm only in charge of the verifier part):)

[Kevin Buzzard]

I think that the answer to your questions are:

Can I use mathlib4 with lean in some way to go over the steps and to check if the theorem are correct?

Yes, but you will have to learn how to use geometry in Lean, and this will involve some work on your part. It will not be impossible but right now there are no good teaching resources. I learnt something about how mathlib handles this kind of mathematics when I reviewed the PR adding this file, which taught me a lot about how Joseph had set things up.

To ask more precisely- are all the basic level geometric Theorem are already implemented in lean4?

Yes. But some of them will be implemented in far more generality than you need, and you will have to understand the difference between things like angles and oriented angles, and whether you are working mod pi or mod 2pi etc. This kind of geometry is more subtle than how it is usually presented to schoolkids and Lean will keep you honest.

If you want some concrete goals, then try stating the question which you want to solve. Use the linked file to help you set up the basics.

[eitan]

Thank you!