|
本帖最后由 hbghlyj 于 2024-11-11 10:50 编辑
见 https://web.archive.org/web/2006 ... b/mm18.pdf/lih0.pdf
“Russian killer” no. 2: A challenging geometric theorem with human and machine proofs
Xiaorong Hou, Hongbo Li, Dongming Wang & Lu Yang
The Mathematical Intelligencer volume 23, pages 9–15 (2001)
Abstract
In February 1998 Sergey Markelov [7] from the Moscow Center for Continuous Mathematics Education sent a set of five geometric theorems to Dongming Wang for testing the capability of his GEOTHER package [8], with the aim of presenting a challenge to computer provers to prove really hard theorems. These theorems have been
used to prepare the Moscow team for the all-Russia school mathematics Olympiad, and are called killers to analytic ways of geometric problem-solving. They can be proved in geometric ways, but no analytic proof could be found even by expert geometers. Let us call these five theorems the Russian killers for short. After a quick look at the five killers,Wang was convinced that some of them can be proved by GEOTHER in principle. For experimental purposes, he took the second of the killers which is stated below.This killer is very easy to explain and to understand, and it provides a beautiful representation of the area of an arbitrary quadrilateral in terms of its four sides and four internal angles.
Theorem.Let $ABCD$ be an arbitrary quadrilateral withsides $AB=k,BC=l,CD=m,DA=n,$and internal angles $2a,2b,2c,2d$ at vertices $A,B,C,D$ respectively; and let $S$ be the area of the quadrilateral. Then\[4 S=\frac{(k+l+m+n)^{2}}{\cot a+\cot b+\cot c+\cot d} -\frac{(l+n-k-m)^{2}}{\tan a+\tan b+\tan c+\tan c}\]The beauty of the expression lies partially at the separation of the sides and internal angles. The theorem generalizes the well-known Brahmagupta formula and the result for the case where the quadrilateral is inscribed a circle.
After a few trials, Wang announced a machine proof of the theorem using Wu's method[10] in GEOTHER in April 1998; this proof requires heavy polynomial computations. Meanwhile, he posted the theorem to several colleagues, soliciting other machine or human proofs. Soon after that, Hongbo Li announced another machine proof using Clifford algebra formalism, followed by the third machine proof given by Lu Yang, both in May 1998. The proofs of Li and Yang are short and took only a few seconds of computing time. Finally in later May 1998, Xiaorong Hou discovered an elegant and short geometric proof of the theorem. This proof reflects the common features of traditional geometric proofs, in which ingenious ideas are used individually to a great extent.
This article collects the four proofs. Its purpose is twofold: on the one hand different kinds of proofs of a difficult geometric theorem are presented that have clear interest for geometers. On the other hand, the proofs show the power and capability of automated deduction methods and tools for proving hard theorems (the Chinese provers against the Russian killers!), and the advantages and disadvantages of machine proofs versus human proofs. From this case study, one is brought to see the machine power and intelligence against human ingenuity in geometric problem solving.
2. A Traditional Geometric Proof
In this section is provided a geometric proof of the theorem worked out by the first author. The non-trivial ideas and special techniques used in the proof, besides their own value, may be a supplement to demonstrate the advantage, significance and power of machine proving, which is automatic, straightforward, and fast.
Let $\Theta=\{a,b,c,d\}$\begin{align*}T & =\frac{k+l+m+n}{2}, & t&=\frac{l+n-k-m}{2} \\ \alpha & =\sum_{\theta \in \Theta} \tan \theta, &\beta &=\sum_{\theta \in \Theta} \cot \theta\end{align*}The formula to be proved becomes$$S=\frac{T^{2}}{\beta}-\frac{t^{2}}{\alpha}$$The proof of the theorem consists of the following five steps.
STEP 1. We first note the following lemma, which is known and can be easily proved.
Lemma 1. If $ABCD$ has an inscribed circle, then$$S=\frac{T^{2}}{\beta}, \quad\abs{A B}=\frac{(\cot a+\cot b) \cdot T}{\beta}$$
'%3E%3Cpath transform='matrix(1.3333 0 0 -1.3333 0 1056)' d='m219.36 335.8h115.4l-17.561 115.4m-80.281-115.4 35.959 107.04m46.831-9.199-71.082-14.217m-29.269-83.625 29.269 83.625m16.307 0h-16.307m-2.927 17.98 2.927-17.98m-2.927 17.98 71.5 13.798' fill='none' stroke='%23000' stroke-miterlimit='10' stroke-width='.335'/%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 311.43 622.65)' font-family='Times' font-size='10.035px' font-style='italic' xml:space='preserve'%3E%3Ctspan x='0' y='0'%3EA%3C/tspan%3E%3Ctspan x='-21' y='0'%3EF%3C/tspan%3E%3Ctspan x='35.122849' y='-121.67559'%3ED %3C/tspan%3E%3Ctspan x='6.2719374' y='-116.65804'%3EC %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 329.16 463.61)' xml:space='preserve'%3E%3Ctspan x='0' y='0' font-family='Courier' font-size='7.5263px'%3E’ %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 314.78 497.77)' xml:space='preserve'%3E%3Ctspan x='0' y='0' font-family='Times' font-size='10.035px' font-style='italic'%3EB %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 323.14 495.11)' xml:space='preserve'%3E%3Ctspan x='0' y='0' font-family='Courier' font-size='8.3626px'%3E’ %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 356.03 503.35)' xml:space='preserve'%3E%3Ctspan x='0' y='0' font-family='Times' font-size='10.035px' font-style='italic'%3EA %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 362.72 500.69)' xml:space='preserve'%3E%3Ctspan x='0' y='0' font-family='Courier' font-size='8.3626px'%3E’ %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 348.23 488.85)' font-family='Times' font-size='10.035px' font-style='italic' xml:space='preserve'%3E%3Ctspan x='0' y='0'%3EI %3C/tspan%3E%3Ctspan x='76.936104' y='99.515076'%3EB %3C/tspan%3E%3Ctspan x='61.464989' y='-23.833363'%3EC %3C/tspan%3E%3Ctspan x='64.392227' y='-7.1078615'%3EE %3C/tspan%3E%3C/text%3E%3C/g%3E%3C/svg%3E)
STEP 2. Let $ABCD$ be an arbitrary quadrilateral. Without loss of generality, we assume that $\abs{BC}+\abs{DA}\ge\abs{AB}+\abs{CD}$ and $\abs{BC}\ge\abs{DA}$. Then one can construct a diagram as in Fig. 2, which yields five points $B^{\prime}, E, F, A^{\prime}, C^{\prime}$, such that
$$
\begin{gathered}
F B^{\prime}\left\|A D, \quad E B^{\prime}\right\| C D, \quad B^{\prime} C^{\prime}\left\|B C, \quad A^{\prime} B^{\prime}\right\| A B \\
|F B|+\left|E B^{\prime}\right|=|B E|+\left|F B^{\prime}\right|=T .
\end{gathered}
$$
So $F B E B^{\prime}$ is inscribed a circle. The details of construction are given in step 5.
STEP 3. In what follows, let $\Delta_{A B C D}$ or $\Delta_{A B C}$ denote the area of an arbitrary quadrilateral $A B C D$ or triangle $A B C$. We have the following corollaries, of which the first two follow immediately from Lemma 1.
so $A^{\prime} B^{\prime} C^{\prime} D$ is inscribed a circle. Moreover,
$$
\Delta_{A^{\prime} B^{\prime} C^{\prime} D}=\frac{t^2}{\alpha}, \quad\left|A^{\prime} B^{\prime}\right|=\frac{(\tan a+\tan b) \cdot t}{\alpha} .
$$
Corollary 1.
$$
\Delta_{F B E B^{\prime}}=\frac{T^2}{\beta}, \quad|F B|=\frac{(\cot a+\cot b) \cdot T}{\beta} .
$$
Corollary 2.
$$
\begin{aligned}
&\left|A^{\prime} B^{\prime}\right|+\left|C^{\prime} D\right|=|A F|+\left|B^{\prime} E\right|-|C D|=|F B|-|A B|+\left|B^{\prime} E\right|-|C D| \\
&=T-(|A B|+|C D|)=t \\
&\left|B^{\prime} C^{\prime}\right|+\left|D A^{\prime}\right|=|C E|+|D A|-\left|F B^{\prime}\right|=|B C|-|B E|+|D A|-\left|F B^{\prime}\right| \\
&=(|B C|+|D A|)-T=t
\end{aligned}
$$
so $A^{\prime} B^{\prime} C^{\prime} D$ is inscribed a circle. Moreover,
Corollary 3. $\Delta_{F A A^{\prime} B^{\prime}}=\Delta_{E C C^{\prime} B^{\prime}}$.
Proof. Let
$$
\gamma=\frac{1}{2} \sin d \cdot \cos b
$$
we have
$$
\begin{aligned}
\Delta_{F A A^{\prime} B^{\prime}} & =\left|A^{\prime} B^{\prime}\right| \cdot\left|F B^{\prime}\right| \cdot \sin 2 a \\
& =\frac{(\tan a+\tan b) \cdot(\cot a+\cot d) \cdot t \cdot T \cdot \sin 2 a}{\alpha \cdot \beta} \\
& =\frac{\sin (a+b) \cdot \sin (a+d) \cdot t \cdot T}{\alpha \cdot \beta \cdot \gamma}, \\
\Delta_{E C C^{\prime} B^{\prime}} & =\left|B^{\prime} C^{\prime}\right| \cdot\left|E B^{\prime}\right| \cdot \sin 2 c \\
& =\frac{(\tan c+\tan b) \cdot(\cot c+\cot d) \cdot t \cdot T \cdot \sin 2 c}{\alpha \cdot \beta} \\
& =\frac{\sin (c+b) \cdot \sin (c+d) \cdot t \cdot T}{\alpha \cdot \beta \cdot \gamma} \\
& =\frac{\sin (\pi-a-d) \cdot \sin (\pi-a-b) \cdot t \cdot T}{\alpha \cdot \beta \cdot \gamma}, \\
& =\Delta_{F A A^{\prime} B^{\prime}} .
\end{aligned}
$$
STEP 4. Note that $I$ is the intersection point of $B^{\prime} E$ and $A^{\prime} D$ in Fig. 2. By Corollary 3, we have
$$
\begin{aligned}
\Delta_{A B C D} & =\Delta_{A B E I}+\Delta_{I E C D} \\
& =\left(\Delta_{F B E B^{\prime}}-\Delta_{F A I B^{\prime}}\right)+\Delta_{I E C D} \\
& =\Delta_{F B E B^{\prime}}-\left(\Delta_{F A A^{\prime} B^{\prime}}+\Delta_{B^{\prime} A^{\prime} I}\right)+\Delta_{I E C D} \\
& =\Delta_{F B E B^{\prime}}-\left(\Delta_{E C C^{\prime} B^{\prime}}-\Delta_{I E C D}\right)-\Delta_{B^{\prime} A^{\prime} I} \\
& =\Delta_{F B E B^{\prime}}-\Delta_{A^{\prime} B^{\prime} C^{\prime} D} .
\end{aligned}
$$
The following theorem is therefore established.
Theorem 1. $\Delta_{A B C D}=\Delta_{F B E B^{\prime}}-\Delta_{A^{\prime} B^{\prime} C^{\prime} D}$.
STEP 5. Construct the diagram in Fig. 3 according to the steps detailed below. It is a simple exercise to verify that the constructed diagram satisfies the requirements given in step 2.
'%3E%3Cpath transform='matrix(1.3333 0 0 -1.3333 0 1056)' d='m199.66 584.08h186.07l-17.561 115.4m-80.281-115.4 35.959 107.04m48.921-24.252-60.628-11.708m-84.462-71.081 84.462 71.081m-112.48-71.081 99.933 83.625m86.134-83.625-86.134 83.625m71.082 14.217-71.082-14.217m-29.269-83.625 29.269 83.625m16.307 0h-16.307m-2.927 17.98 2.927-17.98m-2.927 17.98 71.5 13.798m10.983-77.399c0 20.934-16.99 37.924-37.924 37.924s-37.924-16.99-37.924-37.924 16.99-37.924 37.924-37.924 37.924 16.99 37.924 37.924' fill='none' stroke='%23000' stroke-miterlimit='10' stroke-width='.335'/%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 379.38 291.61)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Times' font-size='10.035px' font-style='italic'%3EA%3C/tspan%3E%3Ctspan x='-19' y='0' fill='%23000000' font-family='Times' font-size='10.035px' font-style='italic'%3EF%3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 295.62 290.62)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Times' font-size='9.617px' font-style='italic'%3EQ %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 262.3 291.05)' fill='%23000000' font-family='Times' font-size='10.035px' font-style='italic' xml:space='preserve'%3E%3Ctspan x='0' y='0'%3EP %3C/tspan%3E%3Ctspan x='122.92998' y='-121.25713'%3ED %3C/tspan%3E%3Ctspan x='94.079063' y='-116.23957'%3EC %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 397.11 132.57)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Courier' font-size='7.5263px'%3E’ %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 382.73 166.73)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Times' font-size='10.035px' font-style='italic'%3EB %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 391.09 164.07)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Courier' font-size='8.3626px'%3E’ %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 423.98 172.31)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Times' font-size='10.035px' font-style='italic'%3EA %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 430.67 169.65)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Courier' font-size='8.3626px'%3E’ %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 518.76 290.5)' fill='%23000000' font-family='Times' font-size='10.035px' font-style='italic' xml:space='preserve'%3E%3Ctspan x='0' y='0'%3EB %3C/tspan%3E%3Ctspan x='-15.471113' y='-123.34844'%3EC %3C/tspan%3E%3Ctspan x='-12.543875' y='-106.62294'%3EE %3C/tspan%3E%3Ctspan x='-11.289488' y='-89.897438'%3EG %3C/tspan%3E%3C/text%3E%3Ctext transform='matrix(1.3333 0 0 1.3333 399.87 186.36)' xml:space='preserve'%3E%3Ctspan x='0' y='0' fill='%23000000' font-family='Times' font-size='9.617px' font-style='italic'%3EH %3C/tspan%3E%3C/text%3E%3C/g%3E%3C/svg%3E)
- Draw the inscribed circle of the three sides $A B, B C, D A$.
- Draw a tangent line $G H$ of the circle that is parallel to line $C D$. This produces a point $G$ on the segment $B C$ and a point $H$ on the segment $D A$.
- Mark off a segment $B P$ of length $T$ and a segment $B Q$ of length $(|A B|+|B G|+|G H|+$ $|H A|) / 2$ on line $B A$ from point $B$.
- Draw the parallel to line $Q H$ through point $P$ that intersects line $B H$ at point $B^{\prime}$.
- Draw the parallel to line $D C$ through point $B^{\prime}$ that intersects line $B C$ at point $E$.
- Draw the parallel to line $D A$ through point $B^{\prime}$ that intersects line $B A$ at point $F$.
- Draw the parallel to line $A B$ through point $B^{\prime}$ that intersects line $D A$ at point $A^{\prime}$.
- Draw the parallel to line $B C$ through point $B^{\prime}$ that intersects line $C D$ at point $C^{\prime}$.
This completes the proof of the theorem.
The geometric constructions used to reduce the problem in the above proof are clearly crucial and well thought out. It is not trivial to figure out such constructions and proofs even for geometry experts. The reader is urged to work out his own geometric proofs. |
|