id: df8a754d7fd64d3d8c52b80b54bd264f
parent_id: 735ad213203f4ed1b82c13ac0cf18fc7
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1709567861259
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"s)\\\n\\\n\"],[-1,\"# Writing todo\\\n~~- Section 2.1:\\\n\\t- Mizar\\\n\\t- Problem representation?~~\\\n- Section 2.2:\\\n\\t- Consistent form for ITP and ATP section, ordering\\\n\\t- Separate comparison section?\\\n- Section 3:\\\n\\t- ~~Mention Mizar efforts? Was also in the early 2000s~~\\\n\\t- work out challenges (a tricolon would be ideal ;)\\\n\\t- clearer mention of SOTA?\\\n- Section 4:\\\n\\t- work out learning methods\\\n\\t- mention currently used tech (MaSh/MeSh for Sledgehammer, k-nn, Naive Bayes for CoqHammer)\\\n- Section 5 intro:\\\n\\t- add good properties of translation (soundness/completeness) + ~~general techniques?~~\\\n\\t- general techniques: ~~type encoding using tags or guards~~, higher-order features (~~lambdas: lifting/combs~~, ..?)\\\n- Section 5.1:\\\n\\t-  cut/summarize notation bit in Isabelle/HOL translation\\\n\\t-  Hoist soundness/performance trade-off bit up to generic translation intro\\\n\\t-  Isabelle/HOL: add more on polymorphism encodings, maybe something on SMT integration\\\n-  Section 5.2:\\\n\\t-  CoqHammer translation\\\n\\t-  CoqHammer results\\\n\\t-  more of a synthesis of the CoqHammer translation; goes into too much detail probably.\\\n-  Section 6:\\\n\\t-  ordering/flow at the end\\\n-  Section 7:\\\n\\t-  write conclusion lol\\\n\\\n\"],[0,\"# Pa\"]],\"start1\":1511,\"start2\":1511,\"length1\":1170,\"length2\":8}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2024-03-04T16:16:05.756Z
created_time: 2024-03-04T16:16:05.756Z
type_: 13