{"entities":{"Q7270083":{"pageid":31062920,"ns":120,"title":"Item:Q7270083","lastrevid":104283782,"modified":"2026-06-25T15:09:31Z","type":"item","id":"Q7270083","labels":{"en":{"language":"en","value":"Formalization of Line Search Methods by Lean"}},"descriptions":{},"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":"Q7270083$F8317A5D-97B1-4849-8B79-E7C81352CE7C","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":"Q7270083$FCD67DBE-2E17-4A64-A431-B71B6993A286","rank":"normal"}],"P21":[{"mainsnak":{"snaktype":"value","property":"P21","hash":"d514d238d7cc09c0b894f838d7f6a042744d62a4","datavalue":{"value":"2606.25412","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7270083$360D8D3B-D48A-4730-96C2-81F394CCE8FB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"93d793763b603421e5dd02a5b6f0d35b92fd0584","datavalue":{"value":"10.48550/arXiv.2606.25412","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7270083$92A98567-69F6-4DF7-86B4-E1002C9085A4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"16b71157143a0fa837af858457844778f457b31e","datavalue":{"value":{"text":"Formalization of Line Search Methods by Lean","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7270083$A7DCF8E2-2902-43B5-BD45-4ED0B5F9415F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7e32322c761499fd2686561dfc03964d97ad4752","datavalue":{"value":{"time":"+2026-06-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7270083$E3AA86BC-1396-4A30-B4E3-12F11A672C91","rank":"normal"}],"P22":[{"mainsnak":{"snaktype":"value","property":"P22","hash":"5a067f3cc35200b51bab0398d603e2eb9779a610","datavalue":{"value":"math.OC","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$46BA9AF0-EB8A-4F20-8C77-0DE25001C25A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P22","hash":"a8be41cbd0f9efc5485d9c5a7cce55a2dc85f5ff","datavalue":{"value":"cs.MS","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$E2C15BF8-B436-4195-A6E9-5B566CD33511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P22","hash":"ebcab1bde8ac3b28efaefc12ea8cc1068c9a8b14","datavalue":{"value":"math.NA","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$39602794-3250-4CD1-9B6F-1B1F99C0244D","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d2405a28bc811698171929a73db8ecccaa4fad71","datavalue":{"value":"Yiyang Zhang","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$8CC332AB-741F-4D43-8751-3C5F0B37301C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"6272ce4fdfc4d0e193ce24a934d25b64ba5e6e94","datavalue":{"value":"Kenneth W. Shum","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$B02911F1-8F50-4C17-967C-4335B0FAC733","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"acc529ecbfc8d6c0bdf0c73afadd707507b93db4","datavalue":{"value":{"entity-type":"item","numeric-id":858284,"id":"Q858284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1642":[{"snaktype":"value","property":"P1642","hash":"a54a2b64f7b8568892d0e11c5b15bda62f19839d","datavalue":{"value":{"entity-type":"item","numeric-id":7270033,"id":"Q7270033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1642"],"id":"Q7270083$ADFE8C5A-1B25-4013-BC7F-4F1C368E7A71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d911c8d8464185908b98b1e7563f5136f5b5276","datavalue":{"value":{"entity-type":"item","numeric-id":517729,"id":"Q517729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1642":[{"snaktype":"value","property":"P1642","hash":"a54a2b64f7b8568892d0e11c5b15bda62f19839d","datavalue":{"value":{"entity-type":"item","numeric-id":7270033,"id":"Q7270033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1642"],"id":"Q7270083$054522C7-4499-43F9-9905-DD3DB3335957","rank":"normal"}],"P1963":[{"mainsnak":{"snaktype":"value","property":"P1963","hash":"2061b378aed6922b185b97f98a3527b01c08c626","datavalue":{"value":"We formalize standard textbook line search methods using Lean 4. This paper provides a comprehensive formalization of fundamental notions and convergence arguments for gradient descent and descent directions, backtracking line search, classical and nonmonotone line search criteria, and the Zoutendijk theorem, advancing machine verification of nonlinear optimization theory.","type":"string"},"datatype":"string"},"type":"statement","qualifiers":{"P1642":[{"snaktype":"value","property":"P1642","hash":"985dbb0e3957a205973fd95bd3fd79ca0980eb5b","datavalue":{"value":{"entity-type":"item","numeric-id":7269921,"id":"Q7269921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1642"],"id":"Q7270083$87A0B4BB-9E68-419A-A1E8-E076B437D4BF","rank":"normal"}],"P1964":[{"mainsnak":{"snaktype":"value","property":"P1964","hash":"4d7221044ede5d0ccc13196b61dab7576833f91c","datavalue":{"value":"Formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$A4794EDB-BACB-4A01-B2A3-CE27FE6EE8FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1964","hash":"eee5d19d6578679616ccf4f7177fb15bc23d632f","datavalue":{"value":"Line Search","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$355B25D7-F27B-4600-99FE-B95EC552B75F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1964","hash":"127f291a4ad4ddd2c3c8aba26f3ce70254d18e06","datavalue":{"value":"Lean 4","type":"string"},"datatype":"string"},"type":"statement","id":"Q7270083$8181A6FC-E261-4257-B23E-29D8AC3F338A","rank":"normal"}],"P1642":[{"mainsnak":{"snaktype":"value","property":"P1642","hash":"a54a2b64f7b8568892d0e11c5b15bda62f19839d","datavalue":{"value":{"entity-type":"item","numeric-id":7270033,"id":"Q7270033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7270083$92DB130F-7E7B-4A00-8E5A-6BC733634458","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of Line Search Methods by Lean","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_Line_Search_Methods_by_Lean"}}}}}