{"entities":{"Q294378":{"pageid":296145,"ns":120,"title":"Item:Q294378","lastrevid":52555823,"modified":"2026-01-22T23:12:18Z","type":"item","id":"Q294378","labels":{"en":{"language":"en","value":"Towards a certified version of the encyclopedia of triangle centers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6593824"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$1C251695-A2A3-422E-9BF4-25D1F36A29DA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7c4966245c06dd51b70fba64db0d42fc643f4b3b","datavalue":{"value":{"text":"Towards a certified version of the encyclopedia of triangle centers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q294378$ADF42EB0-6DED-4A0A-A1FC-60790D1AC380","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9ceda53819a4a7c078a2c43fb84364a7203bfa6a","datavalue":{"value":"1343.51001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q294378$8C05E88A-4798-492C-848F-03CA42AF1916","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7154e8ca53ace223b8c5be019b7f4f775aab0292","datavalue":{"value":{"entity-type":"item","numeric-id":294376,"id":"Q294376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$8CC32DD9-2AAB-46A7-9E71-ADDEFF2960FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"296b44c0c7487db7cf7567934fe97965dd3e319a","datavalue":{"value":{"entity-type":"item","numeric-id":620244,"id":"Q620244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$90ECDBFC-C4D9-414B-9C90-27F0B39DD515","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e5cf57799e8c41ecba181c21bc95047b71cb3443","datavalue":{"value":{"entity-type":"item","numeric-id":294368,"id":"Q294368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$0733E1B5-4432-4938-AECA-070FF3A867A1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b32ada740abbb03089ab30647d244c2741fb6e33","datavalue":{"value":{"time":"+2016-06-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q294378$51AD2504-CAE0-49E1-BA72-256DBDAD39B5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3130d6e44640cfe77176d99a915d9ab5bee3aa9a","datavalue":{"value":"https://hal.inria.fr/hal-01174131/file/certified-etc.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q294378$4B2AB80D-4DCA-4C0E-A1F6-C8778A8762F0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"157f22a007580472c351ff7817bc599e8752e2e2","datavalue":{"value":"A triangle center of a triangle \\(ABC\\) is a point with trilinear coordinates  \\[ f(a, b, c) : f(b, c, a) : f(c, a, b) \\]  where \\(a, b, c\\) denote the side lengths of the triangle \\(ABC\\) and \\(f\\) is a homogeneous function with \\(f(a, b, c) = f(a, c, b)\\). Well-known examples of triangle centers are the center of gravity, the circumcenter, and the orthocenter of a triangle.  The Encyclopedia of Triangle Centers (ETC) contains definitions and many properties of more than 7000 triangle centers. According to the authors, most properties in ETC are given without proof nor reference.  The article presents an effort towards creating a certified version of ETC that provides formal proofs for the properties of the triangle centers.  The authors describe how they use the interactive theorem prover Coq to formalize the definitions and constructions of triangle centers and some of their properties. Since parsing the properties given in ETC appears to be very challenging, the authors instead automatically generate conjectures about collinearity of triangle centers and transformations between triangle centers that can be automatically checked using Coq.  For their Certified Encyclopedia of Triangle Centers (CETC), the authors thus managed to provide formal proofs for almost 80000 properties of 6000 triangle centers.","type":"string"},"datatype":"string"},"type":"statement","id":"Q294378$9B1ED3BF-40B7-4AEF-B90B-E585F50C188B","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"77f82520b0b486fce861b43f8805fa9744a8e398","datavalue":{"value":{"entity-type":"item","numeric-id":590258,"id":"Q590258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$1DD9945E-E64E-463B-8E3D-A2C0B2B48127","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0d8912a48ac60770db1c80088e9517c70dd683cc","datavalue":{"value":"51-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q294378$859F6276-DD93-43CA-B39A-A6764F057E42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q294378$3E7F367B-E6D8-4F64-9627-9E26E1AD6B6E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d6111effc58b130eab73e8ae0bd6c8cd10ce0f0","datavalue":{"value":"6593824","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q294378$228EAE54-CFDA-4140-A36D-4D17D4A1C42D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c381036852f37fcb49123aedec5f335333f08f89","datavalue":{"value":"triangle centers","type":"string"},"datatype":"string"},"type":"statement","id":"Q294378$47F42356-3E91-4182-9E1E-7ED3C7ACDD00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4477c9598ae4965364daa3ce025ec46065fff35c","datavalue":{"value":"geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q294378$51D03B9A-99CC-47DA-8B76-A14A1D41902F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q294378$A1201668-8DE8-4E97-986A-7EBE602EA402","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q294378$EE253055-797F-4944-92FE-C985FDC49C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q294378$FEC0FD68-47DE-4368-9C3D-F632A0D14950","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$F8A84E07-0108-4E45-B61A-98C66AC3D425","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$B502C7D6-123B-4E80-B60E-183B6BB62CC8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c4f6a591f679d51eff9a834d827a96941905d87b","datavalue":{"value":"W2320936035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q294378$E4D64953-53DA-4E03-A733-05374C0673E2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$F1DB5848-814A-47C8-9A23-EF440EC96005","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d45ba0f08d8b9ad108013eb53fd86281684a152c","datavalue":{"value":{"entity-type":"item","numeric-id":2849509,"id":"Q2849509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$C7F7069E-F53C-4B0E-8267-7B3A777D90E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f65b705669c63993345434be77161245f32637c5","datavalue":{"value":{"entity-type":"item","numeric-id":3490991,"id":"Q3490991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$656AA139-9181-4C2D-9A21-06EC173214FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1932306548ebd6723df7c4dea3cd0d797fdf1833","datavalue":{"value":{"entity-type":"item","numeric-id":1924738,"id":"Q1924738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$E503E5AA-63A8-4F75-BEB3-2138A3995721","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9811e0f445518a60fcf8a88a2ec5cd76d23ab843","datavalue":{"value":{"entity-type":"item","numeric-id":5477649,"id":"Q5477649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$5D1F1035-D786-4795-A749-104818216530","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f10bf2b3e1e786082d7e044c9983d3e57e89fcb4","datavalue":{"value":{"entity-type":"item","numeric-id":1394941,"id":"Q1394941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$32F0613C-B2ED-40ED-8CE0-F7DEBFB7B250","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75696de5bc586d56624088f5b34e767f4ec1a83c","datavalue":{"value":{"entity-type":"item","numeric-id":1328237,"id":"Q1328237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$734DE805-BED9-4FD2-B3DC-5A529867536A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0951c142e1ce60b758920d24d51867280a60901","datavalue":{"value":{"entity-type":"item","numeric-id":4763212,"id":"Q4763212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$216AF67C-1306-41D4-A34D-B7CF39E7AAD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7547fb8fede5fb4d98578de033ab0f75c6efa5a1","datavalue":{"value":{"entity-type":"item","numeric-id":4219296,"id":"Q4219296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$240290E4-BF9E-4F66-AE69-D6280690938E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc182df8b38eb530d99faf472b90c793492a26d2","datavalue":{"value":{"entity-type":"item","numeric-id":5453489,"id":"Q5453489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$7C7C4902-C999-4DFD-80A5-0D40DE1245A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17b7b3a7a9d206e650b26a92e6ba562b40aff3b4","datavalue":{"value":{"entity-type":"item","numeric-id":1063634,"id":"Q1063634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q294378$328C1E64-2B94-4F6E-A63B-5BB95B14B6C2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fd7e7aff274774a8ff43c5849d5086d5ce457c76","datavalue":{"value":"10.1007/S11786-016-0254-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q294378$C74AF98A-A46E-4F8B-B469-258A76FFE5C2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0f12a965e8d67a074bd8289137ea0f36193308b","datavalue":{"value":{"entity-type":"item","numeric-id":4219296,"id":"Q4219296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84c0e65b6828c4c893502d7cff15ce4f26512bcd","datavalue":{"value":{"amount":"+0.7669981122016907","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q294378$0BCC892B-0260-4237-84EA-BE35427FD743","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"190ed247c1117e9e9f32b51d16403f5672937424","datavalue":{"value":{"entity-type":"item","numeric-id":4456860,"id":"Q4456860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84c0e65b6828c4c893502d7cff15ce4f26512bcd","datavalue":{"value":{"amount":"+0.7669981122016907","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q294378$E5143C5B-C61C-4544-8145-C3B60C762DA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5a8451ce8b737d7805bdc50adb483dea0577acf","datavalue":{"value":{"entity-type":"item","numeric-id":4763212,"id":"Q4763212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f87088fdd3e9087621252d2c7126d7967eedb1d","datavalue":{"value":{"amount":"+0.7568807601928711","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q294378$17F572D0-5F60-4E12-A3B0-86DF7E020201","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"983d9d68a42d546e297e3d9a9e67c8d72e3ce1ff","datavalue":{"value":{"entity-type":"item","numeric-id":1344004,"id":"Q1344004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f87088fdd3e9087621252d2c7126d7967eedb1d","datavalue":{"value":{"amount":"+0.7568807601928711","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q294378$8C55E2DA-09C7-4F21-BC2C-297AA7886E26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0acd9e188a01babe22481246cc77dcebc2b9d236","datavalue":{"value":{"entity-type":"item","numeric-id":4588196,"id":"Q4588196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7199a0b657faa8ab4e5f5a08fa473bdb0cbaf09","datavalue":{"value":{"amount":"+0.7405415773391724","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q294378$5F190D16-B2C5-44D5-A396-08A0101A5E42","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:294378","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:294378"}}}}}