Continued fractions

Stream: new members

[liu]

屏幕截图 2025-02-09 230600.png
I've encountered a new problem. How can I formalize this problem description?

[Yaël Dillies]

Look at docs#GenContFract

[liu]

How to modify

import Mathlib
example(A: ℝ )(B:ℝ )(C:ℝ )(p:ℝ  )(hp : Nat.Prime p)(x: GenContFract.Pair s)(h1:x=[1;(1,sqrt 2),(1,sqrt 2),...])(h2:B % sqrt p≠0):1*((x+1)*(x-2))⁻¹=(2+sqrt 2)/(-2)∧ |A|+|B|+|C|=2:=by sorry

[liu]

I've encountered a new problem. How can I formalize this problem description?

[liu]

This is my idea .How to modify

import Mathlib
example(A: ℝ )(B:ℝ )(C:ℝ )(p:ℝ  )(hp : Nat.Prime p)(x: GenContFract.Pair s)(h1:x=[1;(1,sqrt 2),(1,sqrt 2),...])(h2:B % sqrt p≠0):1*((x+1)*(x-2))⁻¹=(2+sqrt 2)/(-2)∧ |A|+|B|+|C|=2:=by sorry

[liu]

Who can help me? I don't know if it's a problem with the definitions or something else.

[Yaël Dillies]

Think about the problem in steps:

1. Your x is built as a continued fraction
2. In mathlib, this is called docs#GenContFract
3. To build a GenContFract, you need to build a docs#Stream'.Seq of pairs of real numbers
4. Stream'.Seq (GenContFract.Pair ℝ) is just a wrapper around sequences ℕ → Option (GenContFract.Pair ℝ) with the property that ∀ n, s n = none → s (n + 1) = none (docs#Stream'.IsSeq
5. The ℕ → Option (GenContFract.Pair ℝ) you want is the constant sequence fun _ ↦ (.sqrt 2, 1) (docs#Real.sqrt)
6. Sequences s which don't take the value none obviously respect ∀ n, s n = none → s (n + 1) = none, so mathlib should have that construction
7. That construction is docs#Stream'.Seq.ofStream
8. So you can construct the continued fraction of x as GenContFract.mk 1 (.ofStream fun _ ↦ ⟨.sqrt 2, 1⟩)

[Yaël Dillies]

9. But you want x as a real number, so you need to know how to turn a real number into a continuous fraction
10. This is docs#GenContFract.of
11. You can therefore introduce x and state its property as (x : ℝ) (hx : GenContFract.of x = .mk 1 (.ofStream fun _ ↦ ⟨.sqrt 2, 1⟩))

[Yaël Dillies]

I'll let you do an analogous reasoning for how to introduce A, B, C and state their properties :smile:

[Damiano Testa]

A minor comment: I have usually seen this as continued fractions, not continuous.

[Yaël Dillies]

Do you mean our function $\mathrm{MouthfulNames} \to \mathrm{Abbreviations}$ is not injective? :see_no_evil:

[liu]

This is my idea about how to induce A B C.I don't know if it's correct.

import Mathlib
example(A: ℝ )(B:ℝ )(C:ℝ )(p:ℕ   )(hp : Nat.Prime p)(x: ℝ )(hx : GenContFract.of x = .mk 1 (.ofStream fun _ ↦ ⟨.sqrt 2, 1⟩))
(h2:B % .sqrt p≠0 ∧ 1*((x+1)*(x-2))⁻¹=(A+.sqrt B)/C):1*((x+1)*(x-2))⁻¹=(2+.sqrt 2)/(-2)∧ |A|+|B|+|C|=2:=by sorry

[Yaël Dillies]

Your informal statement says they are integers, so (A: ℝ )(B:ℝ )(C:ℝ ) is definitely wrong

[liu]

You're right.Are there any other mistakes?

[Yaël Dillies]

It would be much easier for me to tell if your lines were at most 100 characters long

[Yaël Dillies]

I don't see anything about B not being divisible by the square of a prime number

[liu]

Is it okay like this?

import  Mathlib
example(A: ℤ )(B:ℤ  )(C:ℤ  )(p:ℕ   )
(hp : Nat.Prime p)(x: ℝ )
(hx : GenContFract.of x = .mk 1 (.ofStream fun _ ↦ ⟨.sqrt 2, 1⟩))
(h2:B % .sqrt p≠0 ∧ 1*((x+1)*(x-2))⁻¹=(A+.sqrt B)/C):
1*((x+1)*(x-2))⁻¹=(2+.sqrt 2)/(-2)∧ |A|+|B|+|C|=2:=by
 sorry

[Yaël Dillies]

You still misinterpreted the condition about B and prime numbers

[liu]

Is it okay like this?

example(A: ℤ )(B:ℤ  )(C:ℤ  )(p:ℕ   )(hp : Nat.Prime p)(x: ℝ )

(hx : GenContFract.of x = .mk 1 (.ofStream fun _ ↦ ⟨.sqrt 2, 1⟩))

(h2:B % (p*p)≠0 ∧ 1*((x+1)*(x-2))⁻¹=(A+.sqrt B)/C):

1*((x+1)*(x-2))⁻¹=(2+.sqrt 2)/(-2)∧ |A|+|B|+|C|=2:=by sorry

[Yaël Dillies]

The condition about B is not about a single prime number, but about all prime numbers. Mathlib spells it as docs#Squarefree

[liu]

Is it okay like this?

import Mathlib
example(A: ℤ )(B:ℤ  )(C:ℤ  )(x: ℝ )(hb:Squarefree B)
(hx : GenContFract.of x = .mk 1 (.ofStream fun _ ↦ ⟨.sqrt 2, 1⟩))
(h2:urefree ∧ 1*((x+1)*(x-2))⁻¹=(A+.sqrt B)/C):
1*((x+1)*(x-2))⁻¹=(2+.sqrt 2)/(-2)∧ |A|+|B|+|C|=2:=by sorry

[Yaël Dillies]

That looks like invalid code

[Luigi Massacci]

@liu I would suggest you do the following to have an easier life:
a) add a line set_option autoImplicit false at the beginning of you code file. It will prevent errors like the one above.
b) stop trying to do everything with an llm, as you seem to be doing in all your threads. They just don’t work this way for lean, they are leading you astray with nonsense and wasting your time

[Luigi Massacci]

and on a less important note, whatever ai you are using formats code like it’s writing a ransom note with newspaper cuttings, which doesn’t help either

[liu]

Is it okay like this?

example(A: ℤ )(B:ℤ  )(C:ℤ  )(x: ℝ )(hb:Squarefree B)

(hx : GenContFract.of x = .mk 1 (.ofStream fun _ ↦ ⟨.sqrt 2, 1⟩))

(h2: 1*((x+1)*(x-2))⁻¹=(A+.sqrt B)/C):

1*((x+1)*(x-2))⁻¹=(2+.sqrt 2)/(-2)∧ |A|+|B|+|C|=2:=by sorry

[liu]

@Luigi Massacci
I know that AI always generates incorrect Lean code, but sometimes I have no other options.

[Yaël Dillies]

Is it not supposed to be (2 + .sqrt 2) / 2 instead?

[Yaël Dillies]

And surely that would make |A| + |B| + |C| = 6 instead of 2, right?

[Yaël Dillies]

No need to have the 1* as well

[liu]

It's (2+.sqrt 2)/(-2)

[Yaël Dillies]

Oh right yes, I agree

[Yaël Dillies]

I would suggest making A B : ℕ to be sure you're not using the fact that Real.sqrt returns 0 on negative inputs

[Chris Wong]

liu said:

Luigi Massacci
I know that AI always generates incorrect Lean code, but sometimes I have no other options.

Where are these problems coming from?

If this is homework, then you would get faster (and correct) help from asking your professor.

[liu]

These questions are from an entrance test on our side. However, Lean isn't widely used in China, and there are too few learning resources available.

[Eric Wieser]

An entrance test for what?

[Chris Wong]

And are you taking the test right now?

[Chris Wong]

The way you're asking questions sounds like you need an answer urgently.

[liu]

enrance test about lean.
Yes,a little urgently

[Eric Wieser]

I meant "what are you trying to enter with this test" - a job, a university course, a secret society...?

[Chris Wong]

I would like to enter the Lean secret society

[liu]

It's a project that aims to formalize and solve mathematical problems using Lean. If you pass this test, you can participate in the project and also get an additional bonus.

[Kevin Buzzard]

So you're saying that if we answer all your questions then you will get a job and then you will ask ten times as many questions? :-/

I think that it would be better for everyone if you stopped using LLMs and started to go through books like #mil . Right now LLMs are not able to do the kind of things which you want, they are not good enough.

[Eric Wieser]

Is this a paid role generating data for an AI company?

[liu]

It is indeed for providing data to build a large mathematical model.

[Eric Wieser]

Can you share which company this project is with?

[liu]

I dont't know.

[Eric Wieser]

To clarify Kevin's comment above; this community is typically very generous with its time to help you learn Lean, but much less so when you are asking others to do homework / exam questions. Perhaps you should try the exam again in a month, and go through more introductory material in the meantime?

[liu]

Okay, not all the questions I ask are from the test. It's not that I'm reluctant to spend time on introductory books. I just think asking experienced people is more efficient than poring over books.
Thank you all for your help.

[Yury G. Kudryashov]

The purpose of an entrance test is to find people who are already good at a job. Usually, you aren't supposed to seek help with your entrance tests or use LLMs to write it for you. Also, if this was for our company, we would consider legal action (but probably drop because we're in different countries) for breaking the NDA.