Automated proving in planar geometry based on the complex number identity method and elimination

Automated proving in planar geometry based on the complex number identity method and elimination | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article Automated proving in planar geometry based on the complex number identity method and elimination Zoltán Kovács, Xicheng Peng This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-7789468/v1 This work is licensed under a CC BY 4.0 License Status: Under Review Version 1 posted 10 You are reading this latest preprint version Abstract We improve the complex number identity proving method to a fully automated procedure, based on elimination ideals. By using declarative equations or rewriting each real-relational hypothesis $h_i$ to $h_i-r_i$, and the thesis $t$ to $t-r$, clearing the denominators and introducing an extra expression with a slack variable, we eliminate all free and relational point variables. From the obtained ideal $I$ in $\mathbb{Q}[r,r_1,r_2,\ldots]$ we can find a conclusive result. It plays an important role that if $r_1,r_2,\ldots$ are real, $r$ must also be real if there is a linear polynomial $p(r)\in I$, unless division by zero occurs when expressing $r$. For higher degree cases of $p(r)$ we suggest further methods to obtain a statement with a proof. We demonstrate the weakness of the original method for testing orthogonality and testing the isosceles property. Our results are presented in Mathematica, Maple and in a new version of the Giac computer algebra system. Finally, we present a prototype of the automated procedure in an experimental version of the dynamic geometry software GeoGebra. Automated theorem prover Complex number identity Elimination Quadratic forms Euclidean geometry GeoGebra Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Under Review Version 1 posted Reviews received at journal 02 Mar, 2026 Reviews received at journal 25 Feb, 2026 Reviews received at journal 21 Feb, 2026 Reviewers agreed at journal 16 Jan, 2026 Reviewers agreed at journal 11 Jan, 2026 Reviewers agreed at journal 09 Jan, 2026 Reviewers invited by journal 07 Jan, 2026 Editor assigned by journal 13 Dec, 2025 Submission checks completed at journal 10 Oct, 2025 First submitted to journal 06 Oct, 2025 You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-7789468","acceptedTermsAndConditions":true,"allowDirectSubmit":false,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":571690501,"identity":"90b3aec6-adef-4474-9796-1726a9c2caa3","order_by":0,"name":"Zoltán Kovács","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAA5klEQVRIiWNgGAWjYFAC5gYgYQNhEqmFsRGoJ410LYdJ0CLf3tj+4OeO83b97O0XHxfusWPglz5+Ab8dPQcbG3vP3E6e2XOm2HjGs2QGyb6cArxamCUSGxt4224nG9zISZPmOcDMYHCGJwGvFjaglsa/beeS7W/kpP/mOVBPWAsPUEszb9sBOwOJ9GPMPAcOA7WwH8CrRYLnYONs2bbkBIkzZ5ilZxw4ziPZw4NXBzDEmg98fNtmZ8/f3v7wc8GBajl+HvYH+PVAQWIDA48B2KUMUAZBYM/AADecSFtGwSgYBaNgxAAAoNlJVac1bWkAAAAASUVORK5CYII=","orcid":"","institution":"Private University College of Education of the Diocese of Linz","correspondingAuthor":true,"prefix":"","firstName":"Zoltán","middleName":"","lastName":"Kovács","suffix":""},{"id":571690502,"identity":"9a55afdb-d3c6-44a3-93f9-6f8307df8f2a","order_by":1,"name":"Xicheng Peng","email":"","orcid":"","institution":"Central China Normal University","correspondingAuthor":false,"prefix":"","firstName":"Xicheng","middleName":"","lastName":"Peng","suffix":""}],"badges":[],"createdAt":"2025-10-06 08:38:28","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-7789468/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-7789468/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":99860968,"identity":"62d7175f-1e2f-4bd7-a3e7-0fb3ff6afeaf","added_by":"auto","created_at":"2026-01-09 07:04:15","extension":"json","order_by":0,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":3928,"visible":true,"origin":"","legend":"","description":"","filename":"1c66cc9d868d46dc99bb3e6b31f124f9.json","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/b2a6bb133d1b935c05908ad5.json"},{"id":99860972,"identity":"9c2f59a0-22f5-4fc4-97f4-ec5dfd5a1b06","added_by":"auto","created_at":"2026-01-09 07:04:15","extension":"png","order_by":1,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":92937,"visible":true,"origin":"","legend":"","description":"","filename":"Ex4.png","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/4ccc4e28d461c9b602f6d1b7.png"},{"id":99860971,"identity":"800baf45-d87d-4dbf-b044-38fda6480d7f","added_by":"auto","created_at":"2026-01-09 07:04:15","extension":"png","order_by":2,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":113822,"visible":true,"origin":"","legend":"","description":"","filename":"Ex5.png","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/b19c436a13b3f37a7023404d.png"},{"id":100357396,"identity":"dcc95ac4-8fa9-4ccf-b5ac-5d4a180d410e","added_by":"auto","created_at":"2026-01-16 07:19:51","extension":"txt","order_by":3,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":133,"visible":true,"origin":"","legend":"","description":"","filename":"cover.txt","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/0d0d2f84aa2f485d30987069.txt"},{"id":100357712,"identity":"b00307a2-6efd-475d-9630-bc330ac1c5cf","added_by":"auto","created_at":"2026-01-16 07:20:14","extension":"cls","order_by":4,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":55331,"visible":true,"origin":"","legend":"","description":"","filename":"snjnl.cls","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/f01395ec1b61446245615300.cls"},{"id":100358028,"identity":"d1d16e93-ec87-40a5-b081-3a9165a4bec1","added_by":"auto","created_at":"2026-01-16 07:20:35","extension":"bst","order_by":5,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":64141,"visible":true,"origin":"","legend":"","description":"","filename":"snmathphysnum.bst","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/dbed0b4e1888fb5d733b5758.bst"},{"id":99860976,"identity":"ddd2554a-70c9-4a18-86bf-7fcedeb6d65d","added_by":"auto","created_at":"2026-01-09 07:04:15","extension":"pdf","order_by":6,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":552015,"visible":true,"origin":"","legend":"","description":"","filename":"submitted.pdf","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/ae75b1d65d1378a323ab6cba.pdf"},{"id":100357274,"identity":"31adc724-daee-46bb-b7c6-6a436a9f8eb7","added_by":"auto","created_at":"2026-01-16 07:19:33","extension":"png","order_by":7,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":76946,"visible":true,"origin":"","legend":"","description":"","filename":"OnlineEx4.png","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/039cabcb805061378d38dbe0.png"},{"id":100357379,"identity":"202d71f7-e199-4b50-bbc5-72b0a942b376","added_by":"auto","created_at":"2026-01-16 07:19:47","extension":"png","order_by":8,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":94886,"visible":true,"origin":"","legend":"","description":"","filename":"OnlineEx5.png","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/c04857dd9a2eeb22f6c654fa.png"},{"id":99860977,"identity":"4540fcc6-2615-4d98-b771-50a9ce5545c2","added_by":"auto","created_at":"2026-01-09 07:04:16","extension":"xml","order_by":9,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":76795,"visible":true,"origin":"","legend":"","description":"","filename":"1c66cc9d868d46dc99bb3e6b31f124f91structuring.xml","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1/eed9a9bb5961ced62bfe4cb6.xml"},{"id":100377217,"identity":"d6a1ff8d-d62a-404c-b4e5-94da1e2fd791","added_by":"auto","created_at":"2026-01-16 08:47:24","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":416041,"visible":true,"origin":"","legend":"","description":"","filename":"submitted.pdf","url":"https://assets-eu.researchsquare.com/files/rs-7789468/v1_covered_c8aace38-2e80-4ac2-9841-787b80c4a57c.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"Automated proving in planar geometry based on the complex number identity method and elimination","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":false,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"annals-of-mathematics-and-artificial-intelligence","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"amai","sideBox":"Learn more about [Annals of Mathematics and Artificial Intelligence](https://www.springer.com/journal/10472)","snPcode":"10472","submissionUrl":"https://submission.springernature.com/new-submission/10472/3","title":"Annals of Mathematics and Artificial Intelligence","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"stoa","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false},"keywords":"Automated theorem prover, Complex number identity, Elimination, Quadratic forms, Euclidean geometry, GeoGebra","lastPublishedDoi":"10.21203/rs.3.rs-7789468/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-7789468/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"\nWe improve the complex number identity proving method to a fully automated procedure, based on elimination\nideals. By using declarative equations or rewriting each real-relational hypothesis $h_i$ to $h_i-r_i$,\nand the thesis $t$ to $t-r$, clearing the denominators and introducing an extra expression\nwith a slack variable, we eliminate all free and relational point variables. From the obtained\nideal $I$ in $\\mathbb{Q}[r,r_1,r_2,\\ldots]$ we can find a conclusive result. It plays an important role\nthat if $r_1,r_2,\\ldots$ are real, $r$ must also be real if there is a linear polynomial $p(r)\\in I$,\nunless division by zero occurs when expressing $r$.\nFor higher degree cases of $p(r)$ we suggest further methods to obtain a statement with a proof.\nWe demonstrate the weakness of the original method for testing orthogonality and testing the isosceles\nproperty. Our results are presented in Mathematica, Maple and\nin a new version of the Giac computer algebra system. Finally, we present a prototype of the automated\nprocedure in an experimental version of the dynamic geometry software GeoGebra.\n","manuscriptTitle":"Automated proving in planar geometry based on the complex number identity method and elimination","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2026-01-09 07:04:11","doi":"10.21203/rs.3.rs-7789468/v1","editorialEvents":[{"type":"communityComments","content":0},{"type":"editorInvitedReview","content":"","date":"2026-03-02T06:24:57+00:00","index":"hide","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2026-02-25T12:28:04+00:00","index":"hide","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2026-02-22T02:13:23+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"38602022504668302978584579112327241845","date":"2026-01-17T03:59:01+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"231091725045636997728788375870365817612","date":"2026-01-11T14:21:28+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"227490283435202994459382420391429155133","date":"2026-01-09T19:40:11+00:00","index":"hide","fulltext":""},{"type":"reviewersInvited","content":"","date":"2026-01-07T19:03:23+00:00","index":"","fulltext":""},{"type":"editorAssigned","content":"","date":"2025-12-13T07:06:51+00:00","index":"","fulltext":""},{"type":"checksComplete","content":"","date":"2025-10-10T13:23:30+00:00","index":"","fulltext":""},{"type":"submitted","content":"Annals of Mathematics and Artificial Intelligence","date":"2025-10-06T08:29:44+00:00","index":"","fulltext":""}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"annals-of-mathematics-and-artificial-intelligence","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"amai","sideBox":"Learn more about [Annals of Mathematics and Artificial Intelligence](https://www.springer.com/journal/10472)","snPcode":"10472","submissionUrl":"https://submission.springernature.com/new-submission/10472/3","title":"Annals of Mathematics and Artificial Intelligence","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"stoa","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false}}],"origin":"","ownerIdentity":"a26171f8-be80-4b35-a828-09cf0369bcba","owner":[],"postedDate":"January 9th, 2026","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"under-review","subjectAreas":[],"tags":[],"updatedAt":"2026-01-09T07:04:11+00:00","versionOfRecord":[],"versionCreatedAt":"2026-01-09 07:04:11","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-7789468","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-7789468","identity":"rs-7789468","version":["v1"]},"buildId":"XKTyCvWXoU3ODBz1xrDgd","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}