Bounding sin(20°)

Stream: new members

[BANGJI HU]

is there simpler way to solve this ? trivial?

import Mathlib


open Real

theorem sin_20_degrees_bounds {pi} :
  (1 / 3 : ℝ) < sin (20 * pi / 180) ∧ sin (20 * pi / 180) < (7 / 20 : ℝ) :=by
constructor
sorry

[Jeremy Tan]

Did you apply to ABAKA?

[Jeremy Tan]

I actually remember doing that exact question as part of my "interview"

[BANGJI HU]

what is ABAKA

[Eric Wieser]

#job postings > Part-Time Lean4 Research Opportunity at ABAKA AI

[BANGJI HU]

anyway dose it can be done by a simple tactic ?for example i can prove 1<2 by trivial

[Kevin Buzzard]

Yes but that's trivial

[BANGJI HU]

import Mathlib


open Real

example:1<2:=by
trivial

theorem sin_20_degrees_bounds {pi} :
  (1 / 3 : ℝ) < sin (20 * pi / 180) ∧ sin (20 * pi / 180) < (7 / 20 : ℝ) :=by
constructor
trivial

[Aaron Liu]

The 1 < 2 is Decidable, so trivial calls decide and evaluates it as true.

[BANGJI HU]

what's the difference

[Michał Mrugała]

Have you tried proving this with pen and paper first?

[Kevin Buzzard]

The difference is that I can prove 1 < 2 from the axioms of mathematics in a few lines, but I cannot even define the sin function from the axioms of mathematics in less than 1000 lines, let alone prove anything about it

[Wang Jingting]

A first thing you might want to know is that currently your code takes pi as a variable (which I assume is not what you want). You can either clarify it as Real.pi and removing the {pi}, or simply use the greek letter when you've opened Real.

[Wang Jingting]

By the way, should this topic be moved to some other section?

[BANGJI HU]

Directly calculate using a calculator: sin(20°) ≈ 0.34202.
Compare: 1/3 ≈ 0.33333, and 7/20 = 0.35000.
Clearly, 0.33333 < 0.34202 < 0.35000.

[Jireh Loreaux]

that's not a proof at all.

[Aaron Liu]

The problem is the ≈, how do you know you've reduced the error bounds enough? I can calculate that since sin(x) ≈ x, therefore sin(0.5) ≈ 0.5 > 0.49 but that doesn't mean sin(0.5) > 0.49. Indeed with a more precise approximation, sin(0.5) ≈ 0.4794 < 0.49.

[Jireh Loreaux]

Some helpful lemmas: docs#Real.sin_le, docs#Real.pi_lt_d2. Can you (hand bob) prove the 7 / 20 bound using those?

[Yury G. Kudryashov]

Jeremy Tan said:

Did you apply to ABAKA?

I suggest that we stop replying to @hand bob 's questions until we get a clear Yes/No answer to this question. Also, please include the following information with each of your questions in the near future:

• a pen&paper proof;
• why are you interested in this particular question?
• what have you tried to solve it in Lean?

[Jz Pan]

In my opinion, asking questions from ABAKA here is considered cheating, because working on these questions is paid.

[Kevin Buzzard]

Yes but experience has shown time and time again that whatever Yury/Eric's opinion is on replying to hand bob, they will continue asking questions and people will continue to answer them.

[BANGJI HU]

and this is not easyone

[Eric Wieser]

Yes indeed, it seems

Jeremy Tan said:

Did you apply to ABAKA?

is indeed not an easy question, since you seem to be avoiding answering it!

[Ilmārs Cīrulis]

I've muted him (hand bob) for now.
Also, TIL about ABAKA.

[Ilmārs Cīrulis]

Although this is interesting exercise (at least to me) to prove, I will keep my mouth shut. :sweat_smile:

[Ilmārs Cīrulis]

Woopie, I did it! :partying_face:
Maybe I should send my resume to ABAKA... :sweat_smile:

[Aaron Liu]

I did it too! The first thing I thought of really worked.

[Ilmārs Cīrulis]

Second part was really easy. In the first I concluded that I don't know how to use derivatives in Lean and proved without them. :D :sweat_smile:

[Aaron Liu]

Fortunately for me I found a way to do it without derivative :smile:

[Ilmārs Cīrulis]

How big (or probably tiny) is your proof?

[Ilmārs Cīrulis]

Mine is 20 lines. Half of them are lemma where I prove some polynomial inequality (instead of using derivative as it should be done, probably :sweat_smile:).

[Aaron Liu]

Ilmārs Cīrulis said:

How big (or probably tiny) is your proof?

From example to done, 11 lines.

[Aaron Liu]

But that might also be influenced by me inlining some tactics.

[Ilmārs Cīrulis]

:open_mouth: Interesting. I believe that your approach should be better than mine.

[Yury G. Kudryashov]

While we're at it, I want to remind that ABAKA is not the only AI firm looking for contractors. Harmonic is looking for contractors too, see #job postings > Harmonic is looking for part-time remote Lean expert

[Ilmārs Cīrulis]

Wow, nlinarith is powerful. Trimmed 6 lines away by using it.