{"entities":{"Q6856411":{"pageid":20635105,"ns":120,"title":"Item:Q6856411","lastrevid":84259331,"modified":"2026-05-14T07:48:13Z","type":"item","id":"Q6856411","labels":{"en":{"language":"en","value":"Exploring proof autoformalization with Mistral on Herald"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8161317"}},"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":"Q6856411$36FFE4BE-D820-45CF-AB49-6319EE3D9F02","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"13c8e3e53295dd86f82a8537c815e791562dd6cc","datavalue":{"value":{"text":"Exploring proof autoformalization with Mistral on Herald","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6856411$E0CCABD4-0809-44CB-8613-A9E6768B91B3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1984321a0ef33ee9d1703fc52489fe98c7931761","datavalue":{"value":"10.1007/978-3-032-07021-0_16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6856411$7DAC26C1-AEDF-4099-A1B3-ADCBF278AAE6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef71b81f71d756ecaa4d466a59b33b5f690a7578","datavalue":{"value":{"entity-type":"item","numeric-id":6856409,"id":"Q6856409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$850F1470-4583-41A7-BEF2-28B1A0008022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f48586c5a41b198e5a25d79b59fc868bcb567d60","datavalue":{"value":{"entity-type":"item","numeric-id":6648156,"id":"Q6648156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$925B4125-16AA-473A-96D1-B2674A5562A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"09927c43cfdba75adab85ad65ab351638195414f","datavalue":{"value":{"entity-type":"item","numeric-id":6538657,"id":"Q6538657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$167D3E9F-FD30-4241-BD41-803E6D646BB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"52590f7511e9da681b9efb7c3af401f5aa529e26","datavalue":{"value":{"entity-type":"item","numeric-id":6856410,"id":"Q6856410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$19A06A29-59E2-46B5-8E0F-94BFFF47A3AE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c0acc3e310b002e7d9eb6bd1bd0a699ed13f8904","datavalue":{"value":{"time":"+2026-02-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6856411$AEDC800C-A7AA-4E08-8D7F-A40BA4D6988A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"51b7800ccceb407b4c9aa81c10252a3a04dbfebf","datavalue":{"value":"68Vxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6856411$07ADB553-987C-42DB-A1F6-40D019999D9A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4c722c61a241305782d78982ddf6aa9056cb00a4","datavalue":{"value":"8161317","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6856411$94D06B22-A790-4997-8538-7E783854C52C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"62ee97b75187c1fc74a439e8fdd1c9b05b918bb8","datavalue":{"value":"autoformalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q6856411$8B7C3B97-63B6-4845-8183-6E2456746207","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e456b0f13edc2f0d00d94a9370fcaa9e0ecbc0d0","datavalue":{"value":"LLM","type":"string"},"datatype":"string"},"type":"statement","id":"Q6856411$1F8EF1A1-344E-419D-954F-789D4D123FC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0eae9dff33adcbc07f74d81a094a208f216c421","datavalue":{"value":"formal math","type":"string"},"datatype":"string"},"type":"statement","id":"Q6856411$FF98ACD7-CDE9-462D-A300-2E68377697AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"240ab882a39c03bf9accf21a95447ae62702e763","datavalue":{"value":"Lean 4","type":"string"},"datatype":"string"},"type":"statement","id":"Q6856411$8F03877D-BB57-4702-AB97-37819706A7BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ece59c48c6b56403e847bffda58343af27541073","datavalue":{"value":"mathlib","type":"string"},"datatype":"string"},"type":"statement","id":"Q6856411$B0E7BE95-6E4D-438A-AAE6-82CFE0172782","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":"Q6856411$930A3085-B0E8-42E3-A1C6-F79932277F1E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1beb980271ff8a0092760ad535401d4b9965bea","datavalue":{"value":{"entity-type":"item","numeric-id":6860025,"id":"Q6860025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$6FC7CA65-0D0F-49F7-9F1D-347EF4EC2B5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdaf319ddaeb6a52a60a91025cb24f95d8069611","datavalue":{"value":{"entity-type":"item","numeric-id":1687711,"id":"Q1687711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$D79DAE9A-5C25-4C85-9FFE-E7207F3B54AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe56c1fd7964c9866b50d41e470eb37047ae3d93","datavalue":{"value":{"entity-type":"item","numeric-id":5495943,"id":"Q5495943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$78C42E96-CC62-41F8-8582-3A20C9F3744D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$F79C79E7-6D10-4515-94E2-B212DDCAE8AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"468fc18a09792dd4a050520bb89e23d01ec79224","datavalue":{"value":{"entity-type":"item","numeric-id":6643010,"id":"Q6643010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$C0557481-6480-4D9C-91E4-D7A779FDFE94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"911abfee84142e554383e3cb062d214f193895b3","datavalue":{"value":{"entity-type":"item","numeric-id":1798975,"id":"Q1798975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6856411$51D4CC4B-7C57-4996-8F42-9E2536D62F31","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Exploring proof autoformalization with Mistral on Herald","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Exploring_proof_autoformalization_with_Mistral_on_Herald"}}}}}